How is the set of all even numbers definable from $\omega$? This Set Theory textbook (page 89) defines definable sets as follows:

Definition 6.8. Given a set $a$ and a formula $\Phi$ we define the formula $\Phi^a$ to be the formula derived
  from $\Phi$ by replacing each occurrence of “$\forall x_i$” in $\Phi$ by an occurrence of “$\forall x_i \in a$”.
Definition 6.9. $b$ is definable from $a$ iff there is a formula $\Phi$ with parameters in $a$ so $b = \{x \in a :
\Phi^a(x)\}$.

Then it proves that the set of even natural numbers is definable from $\omega$ by letting $\Phi$ be the formula $\exists x_0 : x = x_0 + x_0$.
But I am confused: $+$ is not part of the first-order language of set theory (as far as I know), so I am assuming the formula is some kind of abbreviation for a "pure" first-order formula, but I don't know how that formula would look.
My approach is to write a formula that basically says "there exists a function $f$ that satisfies the recursive definition of addition and there is an $x_0$ such that $x = f(x_0, x_0)$", but that doesn't work because $f$ is not in $\omega$.
My other approach is the formula
$$\forall x_0 : \quad [0 \in x_0 \land \forall x_1 : (x_1 \in x_0 \implies S(S(x_1)) \in x_0)] \implies x \in x_0,$$
but it doesn't work because inside $\omega$ there is no set $x_0$ that satisfies the antecedent.
So is the set of even numbers definable, and if so, how?
 A: The set of even numbers is in fact not definable as a subset of $\omega$, considered as a structure in the language of set theory.  Here's one quick way to prove it using a little model theory.  Let me write $<$ for the $\in$ relation, since on $\omega$ this relation is the usual strict total ordering of natural numbers.  By the compactness theorem, there exists a structure $(X,<)$ which is a nontrivial elementary extension of $(\omega,<)$.  For any $x\in X$, define $s(x)$ to be the successor of $y$ with respect to the ordering $<$ (this is definable in terms of $y$, and such a successor always exists in $\omega$ and hence always exists in $X$ by elementary equivalence).
Now consider the map $f:X\to X$ given by $f(x)=x$ if $x\in\omega$ and $f(x)=s(x)$ if $x\not\in\omega$.  Then $f$ is a bijection (since every element except $0$ is the successor of a unique element of $X$), and it is not hard to show that $f$ preserves $<$.  Thus $f$ is an automorphism of the structure $(X,<)$.
Now suppose the even numbers were defined by some formula $\Phi$ with parameters in $\omega$.  Since $f$ fixes every element of $\omega$, $f$ preserves this definition: that is, $\Phi^X(x)$ is true iff $\Phi^X(f(x))$ is true.  But since $\Phi$ defines the even numbers in $\omega$, the sentence $\forall x (\Phi(x)\Leftrightarrow\neg\Phi(s(x)))$ must be true in $\omega$ and hence also in $X$.  Since $f(x)=s(x)$ for any $x\in X\setminus\omega$, this contradicts the fact that $\Phi^X(x)\Leftrightarrow\Phi^X(f(x))$.
