Proof for logical implication : $\exists_x A(x) \rightarrow \forall_x B(x) \implies \forall_x [A(x) \rightarrow B(x)]$ 
Proof for logical implication : $\exists_x A(x) \rightarrow \forall_x B(x) \implies \forall_x [A(x) \rightarrow B(x)]$

Can you please see whether the proof is fine or not?
We know that $ {\forall_x B(x) \implies \exists_x B(x)} \\  [\exists_x A(x) \rightarrow \forall_x B(x)] \implies [\exists_x A(x) \rightarrow \exists_x B(x)] \implies \exists_x  \neg A(x) \lor \exists_x B(x) \implies \\\exists_x [A(x) \rightarrow B(x)]$
Please correct me if I am wrong. I have doubt in that bold alphabet step (can use or not, what happens when we have for all of $x$ in front of $A(x)$. I am doubtful if it is valid or not ... )
$\forall_x A(x) \rightarrow \forall_x B(x) \implies [\forall_x A(x) \rightarrow \exists_xA(x)\rightarrow \forall_x B(x)]  $
Can I say $\forall_x A(x) \rightarrow \forall_x B(x) \implies [ \exists_xA(x)\rightarrow \forall_x B(x)] \implies  \forall_x [A(x) \rightarrow B(x)]$
 A: There is an easy, informal, way to prove that $\exists x A(x) \to \forall x B(x)$ implies $\forall x (A(x) \to B(x))$.
It is well-known that $\exists x A(x) \to C$ is equivalent to $\forall x (A(x) \to C)$, provided that the variable $x$ does not occur free in $C$. 
So, from $\exists x A(x) \to \forall x B(x)$ it follows that 
\begin{align}\tag{1}
\forall x (A(x) \to \forall x B(x))
\end{align}
since $x$ is not free in $\forall x B(x)$.
Now, $(1)$ means that, given an $x$ such that $A(x)$ holds, then $B(y)$ holds for every $y$, in particular for $y = x$. 
Therefore, $\forall x (A(x) \to B(x))$ holds.
We proved that $\exists x A(x) \to \forall x B(x)$ implies $\forall x (A(x) \to B(x))$.
A: The question is:

Can I say $\forall_x A(x) \rightarrow \forall_x B(x) \implies [ \exists_xA(x)\rightarrow \forall_x B(x)] \implies  \forall_x [A(x) \rightarrow B(x)]$

Running the first conditional in a tree proof generator resulted in a countermodel:

Since $A$ is only true for $0$, $\forall x Ax$ is false, but $\exists xAx$ is true. Since $B$ is not true for any members of the domain, $\forall xBx$ is false. This allows the antecedent to be true and the consequent to be false.
A tree proof succeeded for $[ \exists_xA(x)\rightarrow \forall_x B(x)] \implies  \forall_x [A(x) \rightarrow B(x)]$ which is the goal.  
Rather than showing that proof, here is a natural deduction proof in a Fitch-style proof checker. Since this proof checker uses "A" to code universal quantification, I replaced the symbol "A" with "P" and "B" with "Q":

The strategy of the proof was to use the law of the excluded middle (LEM) on $\exists xPx \lor \neg \exists xPx$.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
