I am currently reading Chang and Keisler's model theory textbook, and there is something that I don't seem to be able to understand about their proof (through the Omitting Types Theorem) that every countable model $\mathfrak A = \langle A, E\rangle$ of $ZF$ has an end-elementary extension $\mathfrak B = \langle B, F\rangle$ (Theorem 2.2.18 in the third edition of the book). The main argument is fine, but I don't understand the way in which they apply the axiom of replacement in their proof that a certain theory $T$ locally omits certain types. Here's the part I am having trouble with:


First, they note that a formula $\phi(x, c)$ is consistent with $T$ if and only if 
$$
(\mathfrak A, a)\_{a \in A} \models (\forall y)(\exists z)(\exists x)[z \not \in y \wedge \phi(x, z)].
$$


Then they take an element $a \in A$ and a formula $\phi(x, c)$ (a candidate for locally realizing a certain type which we want to omit) and show that $\phi(x, c) \wedge x \in a$ must be consistent with $T$ - so far so good. Then they claim - and here's where I am stuck: 



> 
> Using the axiom of replacement in ZF, we see in turn that the following sentences hold in $(\mathfrak A, a)\_{a \in A}$: 
>  $$(\forall y)(\exists z)(\exists x)[z \not \in y \wedge \phi(x, z) \wedge x \in a]$$
>  $$(\exists x)(\forall y)(\exists z)[z \not \in y \wedge \phi(x, z) \wedge x \in a]$$
> 
> 
> 


and from the second sentence they conclude that for some $b \in A$, $\phi(b, c) \wedge b \in a$ is consistent with $T$, and the theorem follows easily.


My problem is with the passage from the first sentence, which follows at once from $\phi(x, c) \wedge x \in a$ being consistent with $T$, to the second one, in which $x$ is the same for any choice of $y$. I take it that I have to apply the axiom of replacement here - but how? I can see how to use collection to obtain, from the first sentence, something like 


$$(\exists u)(\forall y)(\exists z)(\exists x)[x \in u \wedge z \not \in y \wedge \phi(x,z) \wedge x \in a];$$


But that's not what the second sentence says, and it is not enough to conclude the proof. 


Chances are that I am forgetting about something bloody obvious, but I've been thinking about this for a couple of days now and I just don't see it. Where is it that I am being stupid?


Thanks!



Replacement axiom and existence of end-extensions (Chang and Keisler's Model Theory)
The negation of the second formula is logically equivalent to
$$\forall x\in a\,\exists y\,\forall z\,(\phi(x,z)\to z\in y).$$
Using collection (and union), this implies
$$\exists y\,\forall x\in a\,\forall z\,(\phi(x,z)\to z\in y),$$
which is equivalent to the negation of the first formula.


