Theorem naecoms

A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)

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