Prove $\forall xA(x) \to B \therefore \exists x(A(x) \to B)$.

Question

Working on P.D. Magnus. "forallX: an Introduction to Formal Logic" (p. 297, exercise C. 1):

$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\}
\def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\}
\def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\}
\def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\}
\def\R#1{\qquad\mathbf{R} \: #1 \\}
\def\ii#1{\qquad\mathbf{\to I} \: #1 \\}
\def\ie#1{\qquad\mathbf{\to E} \: #1 \\}
\def\ne#1{\qquad\mathbf{\neg E} \: #1 \\}
\def\IP#1{\qquad\mathbf{IP} \: #1 \\}
\def\X#1{\qquad\mathbf{X} \: #1 \\}
$
$
\fitch{1.\, \forall xA(x) \to B}{
\fitch{2.\,\neg\exists x(A(x) \to B)}{
\fitch{3.\, A(a)}{
\fitch{4.\, \neg \forall xA(x)}{
\fitch{5.\, \neg A(a)}{
6.\, \bot \ne{3,5}
}\\
7.\, A(a) \IP{5-6}
8.\, \forall xA(x) \Ai{7}
9.\, \bot \ne{4,8}
}\\
10.\, \forall xA(x) \IP{4-9}
11.\, B \ie{1,10}
}\\
12.\, A(a) \to B \ii{3-11}
13.\, \exists x(A(x) \to B) \Ei{12}
14.\, \bot \ne{2,13}
}\\
15.\, \exists x(A(x) \to B) \IP{2-14}
}
$

I am not sure about my use of $\mathbf{\forall I}$ rule on line 7. $A(a)$ is discharged on line 8, but a appears in an open assumption on line 3. Is this proof correct ?

---

EDIT:

From @Graham Kemp answer, I modified the proof to reach this one:

$
\fitch{1.\, \forall xA(x) \to B}{
\fitch{2.\, \neg \exists x(A(x) \to B)}{
\fitch{3.\, A(b)}{
\fitch{4.\, \neg A(a)}{
\fitch{5.\, A(a)}{
6.\, \bot \ne{4,5}
7.\, B \X{6}
}\\
8.\, A(a) \to B \ii{5-7}
9.\, \exists x(A(x) \to B) \Ei{8}
10.\, \bot \ne{2,9}
}\\
11.\, A(a) \IP{4-10}
12.\, \forall xA(x) \Ai{}
13.\, B \ie{1,12}
}\\
14.\, A(b) \to B \ii{3-13}
15.\, \exists x(A(x) \to B) \Ei{14}
16.\, \bot \ne{2,15}
}\\
17.\, \exists x(A(x) \to B) \IP{2-16}
}
$

Answer 1

You are quite correct; that is invalid.

Try building the proof with these assumptions. $$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~\forall x~A(x)\to B}{\fitch{~~2.~\neg\exists x~(A(x)\to B)}{\fitch{~~3.~A(b)}{\fitch{~~4.~\neg A(a)}{\fitch{~~5.~A(a)}{~~\vdots}\\~~\vdots}\\~~\vdots}\\~~\vdots}\\~~~.~\exists x~(A(x)\to B)}$$