Existential quantification as projection

I read the following statement here regarding equivalence of existential quantification and projection of basic relations in model theory.

The operation of taking image under a coordinate projection corresponds to existential quantification while that of taking fibre of coordinate projection corresponds to substituting parameter for variables $\ldots$

I would like to see concrete example of this.

-

Here's a very concrete example:

Suppose we're working with the real numbers in the field language $\langle \mathbb{R},0,1,+,-,\cdot\rangle$.

The formula $\phi(x,y)$ given by $x\cdot x = y$ defines a parabola as a subset of $\mathbb{R}^2$.

Now the formula $\exists x\, \phi(x,y)$ defines as a subset of $\mathbb{R}$ just those values of $y$ which are squares of real numbers, i.e. the nonnegative numbers. You can think of this as projection of the parabola onto the $y$-axis: the image of the projection is those $y$ such that there is some $x$ with $(x,y)$ on the parabola.

On the other hand, the formulas $\phi(x,4)$ defines as a subset of $\mathbb{R}$ just those values of $x$ which square to $4$, i.e. $\{-2,2\}$. You can think of this as the fiber over $4$ of the projection of the parabola onto the $y$-axis: the preimage of $4$ consists of the two points $(-2,4)$ and $(2,4)$.

Now let $T$ be a theory with quantifier elimination, i.e. given any formula, $T$ proves that it is equivalent to one which contains no quantifiers. Suppose $\phi(\overline{x},\overline{y})$ is quantifier-free. Then $\exists \overline{y}\,\phi(\overline{x},\overline{y})$ is the projection of the set defined by $\phi$ onto the $\overline{x}$-coordinate plane. Quantifier elimination tells us that this projection is quantifier-free definable by some formula $\psi(\overline{x})$. So the projection of a quantifier-free definable set is also a quantifier-free definable set.

As a special case, $\text{ACF}_0$, the theory of algebraically closed fields of characteristic $0$, has quantifier elimination. It turns out that the quantifier-free definable sets are exactly the constructible sets in the Zariski topology (finite boolean combinations of polynomial equations). So quantifier elimination tells us that the projection of a constructible set is constructible. This is known as Chevalley's Theorem in algebraic geometry.

Back to the real numbers, if we add the symbol $\leq$ to the language, then $\text{Th}(\langle\mathbb{R},0,1,+,\cdot,\leq\rangle)$ has quantifier elimination. Now the quantifier-free definable sets are exactly the semialgebraic sets (finite boolean combinations of polynomial equations and inequalities). Quantifier elimination tells us that the projection of a semialgebraic set is semiaglebraic. This is known as the Tarski-Seidenberg theorem.

-

Suppose $R(x) \Leftrightarrow \exists y . S(x,y)$. Let $\mathcal{S}$ be the set of pairs $(x,y)$ such that $S(x,y)$. Then $\mathcal{R}$, the set of $x$ such that $R(x)$, is the projection of $\mathcal{S}$ into the first coordinate.

-