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  ax12ev2c  2217  sbequ2  2285  cbv2w  2367  cbv2  2433  cbv2h  2436  axc16i  2466  equvini  2485  equsb2  2522  axsepgfromrep  5247  rext  5416  dfid2  5548  soxp  8139  xpord3inddlem  8164  axextnd  10669  prodmo  16096  mpomatmul  22754  cbvex1v  35697  finminlem  37086  bj-ssbid2ALT  37542  axc11n11  37564  axc11n11r  37565  bj-nnf-cbval  37662  bj-cbv2hv  37689  ax6er  37725  coi1in  37941  bj-dfid2ALT  37960  bj-imdiridlem  38086  wl-axc11rc11  38495  poimirlem25  38543  axc11nfromc11  39963  aev-o  39968  oppcendc  50095