mathematical logic: a step is not clear 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.
 A: But why does Shoenfield seemingly refer to the first move as "Bringing the left hand side into prenex form"? The left-side is in prenex form already. The operation of dragging the negation of the front Is not making it prenex (by his own standards).
I agree completely. I think he actually wanted to write something like: "Bringing the left side to the step precedeing the prenex form [i.e. the inversion of prenex operation (b) on page 37, and assuming, with this, the opening of A - see in this respect the use of the theorem (1) in relation to an open formula in the following Herbrand's theorem]".
A mystery why he writes that?
Of course, the mystery will not be solved by the author, since he's gone.
A: [Corrected version, after comments!]
Evidently $\exists x \neg A \to \neg A_x[\mathbf{r}]$ is an axiom. Bring the quantifier to the front on the l.h.s. and we have
$$\vdash_T \neg \forall x A \to \neg A_x[\mathbf{r}]$$ 
and contraposing (which we allowed to do by "using the tautology theorem") we get
$$\vdash_T A_x[\mathbf{r}] \to \forall x A$$ 
But why does Shoenfield seemingly refer to the first move as "bringing the left hand side into prenex form"? The left-side is in prenex form already. The operation of dragging the negation of the front isn't making it prenex (by his own standards). A mystery why he writes that?
