= Solution
Choose a fresh variable $x_3$. In A7 take the equality antecedent $x_3=x_1$, the atomic formula $\phi=(x_3=x_2)$, and replace its occurrence of $x_3$ by $x_1$. This gives directly the theorem
$$
\vdash x_3=x_1\to(x_3=x_2\to x_1=x_2).
$$
Generalize on $x_3$, with no open assumptions. A4 then instantiates that <quantifier> with the term $f(x_0)$. The substitution is free for $x_3$, since the matrix contains no <quantifiers>. One modus-ponens step yields
$$
\vdash f(x_0)=x_1\to(f(x_0)=x_2\to x_1=x_2).
$$
Finally generalize, in order, on $x_2$, $x_1$, and $x_0$. The result is
$$
\boxed{\vdash\forall x_0\forall x_1\forall x_2\,[f(x_0)=x_1\to(f(x_0)=x_2\to x_1=x_2)].}
$$
Every step is A7, <universal generalization rule>[generalization], A4, or <modus ponens rule>[modus ponens]. Neither completeness, adequacy, nor an unproved appeal to all propositional <tautologies> is needed. In particular the proof does not silently upgrade the variable-only equality axiom to an arbitrary-term axiom: quantification and instantiation perform that upgrade explicitly.
Back to article page
