Theorem alequcom 1495

Description: Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 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	⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Proof of Theorem alequcom

Step	Hyp	Ref	Expression
1		ax-10 1483	1 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)

Syntax hints:   → wi 4  ∀wal 1329

This theorem was proved from axioms:  ax-10 1483

This theorem is referenced by:  alequcoms  1496  nalequcoms  1497  aev  1784