Theorem equcomi 2050

Description: Commutative law for equality. Equality is a symmetric relation. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 10-Jan-1993.) (Revised by NM, 9-Apr-2017.)

Assertion

Ref	Expression
equcomi	⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Proof of Theorem equcomi

Step	Hyp	Ref	Expression
1		equid 2045	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2049	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥))
3	1, 2	mpi 21	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  equcom  2051  equcoms  2053  ax13dgen2  2175  sbequ2  2286  cbv2w  2368  cbv2  2434  cbv2h  2437  axc16i  2467  equvini  2486  equsb2  2523  axsepgfromrep  5253  rext  5427  dfid2  5556  soxp  8131  xpord3inddlem  8156  axextnd  10604  prodmo  16029  mpomatmul  22674  cbvex1v  35591  finminlem  36945  bj-ssbid2ALT  37401  axc11n11  37423  axc11n11r  37424  bj-nnf-cbval  37521  bj-cbv2hv  37548  ax6er  37584  bj-dfid2ALT  37817  bj-imdiridlem  37945  wl-axc11rc11  38354  poimirlem25  38402  axc11nfromc11  39807  aev-o  39812  oppcendc  49952