Problem in Logic - Hilbert Systems

[andrewkirk]

Homework Statement

In a Hilbert System, prove:
\phi[x|m] \rightarrow\forall y((y=m)\rightarrow\phi[x|y])
where \phi is a formula, y, x are variables and m is a constant.
\phi[a|b] denotes the formula obtained by substituting b for a in \phi
This problem crops up in my attempting to prove Godel's diagonal lemma (aka 'Fixed Point Theorem').

Homework Equations

The axioms of a Hilbert system are standard, as set out in http://en.wikipedia.org/wiki/Hilbert_system

The Attempt at a Solution

\begin{align}
\phi[x|m]\ \ \ \ \ \ \text{1. Hypothesis}\\
y=m\ \ \ \ \ \ \text{2. Hypothesis}\\
(y=m)\rightarrow(\phi[x|m]\rightarrow\phi[x|y))\ \ \ \ \ \ \text{3. Axiom Schema 6 (substitution of equal variables)}\\
\phi[x|m]\rightarrow\phi[x|y]))\ \ \ \ \ \ \text{4. Modus Ponens applied to 2 and 3}\\
\phi[x|y]\ \ \ \ \ \ \text{5. Modus Ponens applied to 1 and 4}\\
(y=m)\rightarrow\phi[x|y]\ \ \ \ \ \ \text{6. Deduction Theorem applied to 2 and 5)}\\
\phi[x|m]\rightarrow((y=m)\rightarrow\phi[x|y])\ \ \ \ \ \ \text{7. Deduction Theorem applied to 1 and 6)}\\
\end{align}
This is almost what's required, except it's missing the universal quantifier \forall y and I can't use Axiom Schema 4 of Generalisation to add it because y is free in this formula.
I tried a different approach that gave me the quantifier where I needed it, but it didn't have the right form.

Any suggestions gratefully received.

PS the equations are horribly aligned. Any suggestions about how to better align them in TeX would be appreciated too.