Theorem alequcom 1140

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	⊢ (∀x x = y → ∀y y = x)

Proof of Theorem alequcom

Step	Hyp	Ref	Expression
1		ax-10 964	1 ⊢ (∀x x = y → ∀y y = x)

Syntax hints:   → wi 3  ∀wal 952   = wceq 954

This theorem is referenced by:  alequcoms 1141  nalequcoms 1142  aev 1206  ax11indalem 1366  a12stdy2 1371  axrepnd 4938

This theorem was proved from axioms:  ax-10 964

Copyright terms: Public domain