I'm reading the Shoenfield's book Mathematical Logic. On page 53 it states:
Let r be the special constant for $\exists x.\neg$A. Then $\exists x. \neg A \implies \neg A_x[\boldsymbol{r}]$ [substitution of r for x] is an axiom of $T_c$. Bringing the left-hand side to prenex form and using the tautology theorem,
$⊢_{T_c} A_x[\boldsymbol{r}] \implies\forall x. A.$
I do not understand why the author refers to prenex form. Someone can explain? Thank you.