Theorem axc11n

Derive set.mm's original [ax-c11n] from others. Commutation law for identical variable specifiers. The antecedent and consequent are true when \( x \) and \( y \) are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). If a disjoint variable condition is added on \( x \) and \( y \), then this becomes an instance of aevlem. Use aecom instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Revised by Wolf Lammen, 30-Nov-2019.) (Proof shortened by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 2-Jul-2021.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, x = y \rightarrow \forall y \, y = x \)
Proof
dveeq1
l1
com12 _
\( \vdash x = z \rightarrow \neg \forall y \, y = x \rightarrow \forall y \, x = z \)
l2
axc11r
\( \vdash \forall x \, x = y \rightarrow \forall y \, x = z \rightarrow \forall x \, x = z \)
aev
\( \vdash \forall x \, x = z \rightarrow \forall y \, y = x \)
syl6 l2 _
\( \vdash \forall x \, x = y \rightarrow \forall y \, x = z \rightarrow \forall y \, y = x \)
l5
syl9 l1 _
\( \vdash x = z \rightarrow \forall x \, x = y \rightarrow \neg \forall y \, y = x \rightarrow \forall y \, y = x \)
ax6evr
\( \vdash \exists z \, x = z \)
exlimiiv l5 _
pm2.18d _