Theorem equcomi 1126

Description: Commutative law for equality. Lemma 7 of [Tarski] p. 69.

Assertion

Ref	Expression
equcomi	⊢ (x = y → y = x)

Proof of Theorem equcomi

Step	Hyp	Ref	Expression
1		equid 1124	. 2 ⊢ x = x
2		ax-8 962	. 2 ⊢ (x = y → (x = x → y = x))
3	1, 2	mpi 44	1 ⊢ (x = y → y = x)

Syntax hints:   → wi 3   = wceq 954

This theorem is referenced by:  equcom 1127  equcoms 1128  equtr2 1131  ax10 1139  cbv2 1161  equvini 1166  equsb2 1192  aev 1206  a16g 1274  axsep 2697  rext 2749  ider 4259  unxpdomlem 4823  axextnd 4923

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-8 962  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

Copyright terms: Public domain