= Solution
Use the <equality introduction rule> to prove $t_1=t_1$. In the <equality elimination rule>, choose the <first-order formula> $\phi(z)$ to be $z=t_1$. Substituting $t_2$ for $t_1$ in its first position proves symmetry:
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $t_1=t_2$
| Premise
| 2
| $\{1\}$
| $t_1=t_1$
| <equality introduction rule> $=\text{-intro}$
| 3
| $\{1\}$
| $t_2=t_1$
| <equality elimination rule> $=\text{-elim}$ on 1, 2
Thus $\boxed{t_1=t_2\vdash t_2=t_1}$. This uses only the two supplied equality rules; symmetry has not been assumed as an additional rule.
Back to article page
