That is a central point about automatic structures: By projection (“existential quantification”) you get another regular predicate, and regular predicates are also closed under intersection and complementation. Consequently, the first-order theories of automatic structures are decidable (because you can decide for a given automaton whether he accepts any word).

The proof is quite simple: You want to project $x$ away—just simulate every possible input for $x$ in parallel using sets of states of the old automaton as states for the new automaton (it remains a finite state machine, since the power set of a finite set is finite).

As conjectured above you can also prove it using the MSO translation, let me sketch it: You have regular predicate $R(x,y)$ defined using a MSO formula. This MSO formula uses relation symbols $X_{(a,b)}$ to refer to “the set of positions where $x$ has character $a$ and $y$ has character $b$”. For the projection add existential second-order quantifiers $\exists Q_1\ldots Q_n$ (where $\Sigma=\left\{1,\ldots,n\right\}$) and replace the occurencesof $X_{(a,b)}$ by $X_b\wedge Q_a$ and add an expression expressing that the sets $Q_a$ build a partition. This is not yet correct, because it does not consider different lengths of $x$ and $y$ and we have to deal with some trailing characters, but that is as easy. However–the whole MSO-based proof is much more complicated than constructing an automaton directly.

Notice that both proofs can be transfered to $\omega$-automata and finite and infinite tree-automata.