predicate logic proof about not free variable The question is 

Prove that $\vdash (\forall x_i(A\to B)\to(\exists x_i A\to B)$ for any formulas A, B provided that the variable $x_i$ does not occur free in B.

Can someone help me sketch this proof? 
 A: We can prove it using Enderton's axiom system : see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)) [page 112] :

  
*
  
*Tautologies(in the sense of propositional logic);
  
*$∀ x α →α^x_
t $, where $t$ is substitutable for $x$ in $α$ ($α^x_
t$ is the formula derived from $\alpha$ by replacing $x$ by a term $t$);
  
*$∀ x(α→β)→( ∀ x α→∀x β)$;
  
*$α→∀x α$, where $x$ does not occur free in $α$.
  
  
  modus ponens is the only rule of inference.

Proof
1) $\forall x (A \rightarrow B)$ --- assumed [a]
2) $A \rightarrow B$ --- from Ax.2 and 1), by modus ponens
3) $\lnot B \rightarrow \lnot A$ --- from 2) by tautological implication (with the tautology : $(p \rightarrow q) \leftrightarrow (\lnot q \rightarrow \lnot p)$)
4) $\lnot B$ --- assumed [b]
5) $\lnot A$ --- from 3) and 4) by mp
6) $\forall x \lnot A$ --- from 5) and GENERALIZATION THEOREM [page 117] ($x$ is not free in assumptions [a] nor in assumption [b], because $x \notin FV(B)$)
7) $\lnot \exists x A$ --- from 6) by abbreviation : $\exists$ stands for $\lnot \forall \lnot$, see page 68
8) $\lnot B \rightarrow \lnot \exists A$ --- from 4) and 7) by Deduction Theorem [see page 118], "discharging" assumption [b]
9) $\exists A \rightarrow B$ --- from 8) by tautological implication (see 3)

10) $\forall x (A \rightarrow B) \rightarrow (\exists A \rightarrow B)$ --- from 9) by Deduction Theorem.


The proof is a little bit shorter with Natural Deduction : with it we can avoid the two tautological implication steps, using $\exists$-elimination.
