Theorem aecoms

A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)

Hypothesis
aecoms.1
\( \vdash \forall x \, x = y \rightarrow \varphi \)
Conclusion
\( \vdash \forall y \, y = x \rightarrow \varphi \)
Proof
l0
aecom
\( \vdash \forall y \, y = x \leftrightarrow \forall x \, x = y \)
aecoms.1
\( \vdash \forall x \, x = y \rightarrow \varphi \)
sylbi l0 _