Theorem alequcom 1568

Description: 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). (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
alequcom	|- ( A. x x = y -> A. y y = x )

Proof of Theorem alequcom

Step	Hyp	Ref	Expression
1		ax-10 1558	1 |- ( A. x x = y -> A. y y = x )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-10 1558

This theorem is used by:  alequcoms  1569  nalequcoms  1570  aev  1865