Does this prove the validity of this First Order Logic formula? Is this a valid proof for the following problem?
Prove:
$$\models (\exists x : A(x) \to \forall x : B(x)) \to \forall x : (A(x) \to B(x))$$
Proof by contradiction:


*

*Assume $(\exists x: A(x) \to \forall x : B(x)) \land \lnot (\forall x(A(x) \to B(x))$

*$ (\lnot \exists x : A(x) \lor \forall x : B(x)) \land \lnot\forall x : (A(x) \to B(x))$  logical equivalence

*$\forall x : \lnot A(x) \lor \forall x : B(x)) \land \lnot(\forall x : (A(x) \to B(x))$  logical equivalence

*$\lnot A(a) \lor B(a) \land \lnot((A(a) \to B(a))$          instantiation

*$((A(a) \to B(a)) \land \lnot((A(a) \to B(a))$          a contradiction
$\therefore (\exists x: A(x) \to \forall x : B(x)) \to \forall x(A(x) \to B(x))$ 
Edit: corrected a typo on step 2
Update: Professor's Solution:


*

*Assume $(\exists x: A(x) \to \forall x : B(x)) \land \lnot (\forall x(A(x) \to B(x))$

*$ (\lnot \exists x : A(x) \lor \forall x : B(x)) \land \lnot\forall x : (A(x) \to B(x))$  logical equivalence

*$ (\lnot \exists x : A(x) \lor \forall x : B(x)) \land \lnot\forall x : (\lnot A(x) \lor B(x))$  logical equivalence

*$ ( \forall x : \lnot A(x) \lor \forall x : B(x)) \land \lnot\forall x : (\lnot A(x) \lor B(x))$  logical equivalence

*$ ( \forall x : \lnot A(x) \lor \forall x : B(x)) \land \exists x : \lnot(\lnot A(x) \lor B(x))$  logical equivalence

*$ ( \forall x : \lnot A(x) \lor \forall x : B(x)) \land \exists x : ( A(x) \land \lnot B(x))$  distribute negation

*$ ( \lnot A(a) \lor B(a)) \land ( A(a) \land \lnot B(a))$  instantiation

*$ ( \lnot A(a) \lor B(a)) \land ( \lnot A(a) \lor B(a))$  logical equivalence, resulting in a contradiction


$\therefore (\exists x: A(x) \to \forall x : B(x)) \to \forall x(A(x) \to B(x))$
What I learned: it is typically safe to instantiate when there is one existential quantifier, which is not negated.
 A: In step 2 you make use of the equivalence 
$\neg(\exists x . A(x) \lor \forall x.B(x)) \iff \forall x . \neg A(x) ∨ \forall x . B(x) $
This is not a real equivalence compare it to demorgans law.
$\neg(\exists x . A(x) \lor \forall x.B(x)) \iff \neg(\exists x . A(x)) \land \neg(\forall x.B(x))$
A: Step 4 is wrong! 
It looks like you instantiated all universals with an $a$, but you cannot do that when the universals are part of a larger sentence.
Consider: Suppose you have 
$$\neg \forall x \ P(x) \land \neg \forall x \ \neg P(x)$$
Now, if we are allowed to just instantiate each of these universals with an $a$, we would get $\neg P(a) \land \neg \neg P(a)$, which is a contradiction. But, the orginal statement is not a contradiction at all; if we interpret $P(x)$ as '$x$ is even', and the domain is all numbers, then the original statement is obviously true.
Even more fundamentally, if you have $\neg \forall x \ P(x)$, you cannot fill in anything you want. Using the same interpretation as before, it is clear that $\neg \forall x \ P(x)$ is true, but $\neg P(0)$ is not. So, you cannot instantiate a universal with anything you wany if it is being negated, but this is what you did when in step 4 you went from $\neg \forall x (A(x) \rightarrow B(x))$ to $\neg (A(a) \rightarrow B(x))$
Step 2 is also wrong. The result of rewriting  the conditional as an implication should be:
$(\neg \exists x \ A(x) \lor \forall x \ B(x)) \land \neg \forall x (A(x) \rightarrow B(x))$
Interestingly, given your step 2, step 3  is also wrong, as pointed out by @QthePlatypus, but with this corrected step 2, your step 3 actually would follow ... so maybe this was just a typo on your part?
A: If you want a syntactic proof for a conditional statement, I suggest that you should use a Conditional Proof format.
So assume $\exists x~A(x)\to\forall x~B(x)$ and do something to derive $\forall x~(A(x)\to B(x))$. 
Then discharge the assumption with conditional introduction.
$\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}}
\fitch{}{\fitch{1.~\exists x~A(x)~\to~\forall x~B(x)}{\fitch{~\ldots}{~\ddots}\\8.~\forall x~(A(x)\to B(x))}\\9.~(\exists x~A(x)\to\forall x~B(x))\to\forall x~(A(x)\to B(x))}$
