prenex normal form and "free" variables $∀Y ((∀Xp(X, Y )) → ∃Zq(X, Z))$ 
I am trying to convert the above formula into prenex normal form. I have done the following, but my answer seems to slightly differ from the correct answer:
$∀Y ((\neg \forall X \; p(X, Y )) \lor ∃Z \;q(X, Z))$ (implication elimination)
$∀Y ((\exists X \; \neg p(X, Y )) \lor ∃Z \;q(X, Z))$ (Definition of $\exists$)
$∀Y\exists X  ((\neg p(X, Y )) \lor ∃Z \;q(X, Z))$ (Pull the existential $X$ quantifier out)
$∀Y\exists X\exists Z  ((\neg p(X, Y )) \lor q(X, Z))$ (Pull the existential $Z$ quantifier out)
However, the answer is: $∀Y ∃T∃Z(¬p(T, Y ) ∨ q(X, Z))$
Now I suspect it might be something to do with free variables, but I don't exactly know what I've done wrong. How come the $X$ turns into a $T$? 
 A: The $X$ in the consequent $\exists Z\,q(X,Z)$ is free. The $X$ quantifier in the antecedent $\forall X\,p(X,Y)$ does not bind it. That free $X$ has nothing to do with the bound $X$ in $\forall X\,p(X,Y)$. It's just a coincidence (an unfortunate one) that they're the same variable.
However, in your third step, you move $\exists X$ to the outside without changing it to a fresh variable. In doing that, you capture the $X$ that's free in $\exists Z\,q(X,Z)$. This changes the meaning of the formula, and the resulting formula is not logically equivalent to previous formula.
Another approach would be to change the free variable $X$ in the consequent to another, new variable before moving the $\exists X$ quantifier to outer scope, in order to not capture the free $X$ in $\exists Z\,q(X,Z)$. That would result in, for example,
$$\forall Y\,(\forall X\,p(X,Y) \to \exists Z\,q(S,Z))
$$
One or the other occurrence of $X$ has to be changed to a fresh variable, otherwise you change the meaning of the formula and don't preserve logical equivalence when moving quantifiers.
