Hi guys. I came up with a "proof" for $\displaystyle \vdash(\exists x)Ax\to (y)Ay$, where $\displaystyle Ax$ is a prime formula, which is obviously false. But what have I done wrong?

I'm using Church's first pure predicate calculus formulation, $\displaystyle F^1$ (found in §30).

Suppose $\displaystyle Ax$ is a prime formula. Then

(1) $\displaystyle \neg Ax$ - premise

(2) $\displaystyle (x)\neg Ax$ - generalization (Church *301, §30).

Therefore $\displaystyle \neg Ax\vdash (x)\neg Ax$. By the deduction theorem (Church *360, §36), it follows that $\displaystyle \vdash (\neg Ax)\to(x)\neg Ax$. So

(3) $\displaystyle (\neg Ax)\to(x)\neg Ax$ - theorem (from above)

(4) $\displaystyle ((\neg Ax)\to (x)\neg Ax)\to((\neg(x)\neg Ax)\to\neg \neg Ax)$ - axiom (Church *304, §30)

(5) $\displaystyle (\neg(x)\neg Ax)\to\neg \neg Ax$ - 3,4,mp

(6) $\displaystyle ((\exists x) Ax)\to\neg \neg Ax$ - 5, def. of $\displaystyle \exists$

(7) $\displaystyle ((\exists x) Ax)\to Ax$ - 6, equ. of $\displaystyle \neg\neg$

(8) $\displaystyle (\exists x) Ax$ - premise

(9) $\displaystyle Ax$ - 7,8,mp

(10) $\displaystyle (x)Ax$ - 9, generalization (Church *301, §30)

(11) $\displaystyle (x)Ax\to Ay$ - axiom (Church *306, §30)

(12) $\displaystyle Ay$ - 10,11,mp

(13) $\displaystyle (y)Ay$ - 12, generalization (Church *301, §30).

So $\displaystyle (\exists x)Ax\vdash(y)Ay$, which by the deduction theorem (Church *360, §36) means $\displaystyle \vdash(\exists x)Ax\to (y)Ay$. But clearly this is false! So where did I go wrong?

Thanks in advance!