Is Unification "an Implementation of Existential Quantification"?
It's possible you're paraphrasing me. I've certainly said things similar to that e.g. here.

A more precise statement would be that existential quantification in logic programming languages is (typically) handled by introducing a unification variable. To perform existential introduction, you need to have a term $t$. The rule looks like: $$\dfrac{\Gamma\vdash P[t/x]}{\Gamma\vdash\exists x.P}$$

One way to implement this is to just guess a term $t$ and then see if we can backchain $P(t)$. Of course, for a language like Prolog, there are an infinite number of possible terms, and you have no guidance on what term to guess. A different option is to have $t$ be a meta-variable that stands for a term and continue execution on the hope that we can constrain $t$ enough to know what to decide later. This is essentially what a unification variable is. Unification itself just constrains what possible terms that meta-variable can be. Then, instead of actually enumerating the (now constrained) terms, we usually return the (simplified) constraints themselves as a compact representation of the set of possible terms, assuming they aren't contradictory (i.e. that that set isn't empty).

The occurs-check is simply the enforcement of the fact that usual term languages don't have infinite terms. You can consider other term languages that can represent these terms leading to things like rational tree unification.

Unsurprisingly, the operation unification itself most directly implements is equality. If we did the "exhaustively enumerate terms" approach to handling existential quantification, all the places where we (implicitly) use "unification" could just be straightforward syntactic checks of ground terms. With meta-variables, they instead produce constraints. Of course, this suggests the natural and common generalization of allowing constraints other than syntactic equality, and this leads to constraint logic programming. One generic example of such a constraint is disunification which states what a term (potentially containing meta-variables) cannot be. It is the negation of unification, $t\not\equiv s$ states that for all substitutions $\sigma$, $t[\sigma]\neq s[\sigma]$.