Past exam of the logic and set theory course of the University of Oxford / 2009 / A / 2 / d / Solution

Choose a fresh variable $x_3$. In A7 take the equality antecedent $x_3=x_1$, the atomic formula $\varphi =(x_3=x_2)$, and replace its occurrence of $x_3$ by $x_1$. This gives directly the theoremGeneralize 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 yieldsFinally generalize, in order, on $x_2$, $x_1$, and $x_0$. The result isEvery step is A7, generalization, A4, or 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.