Theorem alequcom 1138

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).

Assertion

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

Proof of Theorem alequcom

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

Syntax hints:   -> wi 3  A.wal 951   = wceq 953

This theorem is referenced by:  alequcoms 1139  nalequcoms 1140  aev 1204  ax11indalem 1361  a12stdy2 1366  axrepnd 4918

This theorem was proved from axioms:  ax-10 963

Copyright terms: Public domain