I am stuck on this one, I know I have to use Ax3 which is $$(\forall x)(A\to B)\to(\exists x)A\to(\exists x)B$$ and convert the existential quantifier to universal, but I have problem making it to become just as Ax3
The original was just like the following:
Show that |- $(\forall x)(A\to B)\to(\exists x)A\to(\exists x)B$
Hint: Use the definition of existential quantifier to eliminate ∃
I don't think you can use Ax3 to prove that property. I don't know what rules you're allowed to use, but I would do the following: Assume that $\forall x (A \implies B)$ and $\exists x A$. Then eliminate the existential to get some particular $A$. Then apply $\forall x (A \implies B)$ to get a particular $B$. Then use this $B$ as the witness to the final existential.