Theorem equcomi 2049

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 2044	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2048	. 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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

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

This theorem is used by:  equcom  2050  equcoms  2052  ax13dgen2  2174  ax12ev2c  2216  sbequ2  2284  cbv2w  2366  cbv2  2432  cbv2h  2435  axc16i  2465  equvini  2484  equsb2  2521  axsepgfromrep  5246  rext  5415  dfid2  5547  soxp  8145  xpord3inddlem  8175  axextnd  10681  prodmo  16110  mpomatmul  22768  cbvex1v  35752  finminlem  37200  bj-ssbid2ALT  37656  axc11n11  37678  axc11n11r  37679  bj-nnf-cbval  37776  bj-cbv2hv  37803  ax6er  37839  bj-dfid2ALT  38086  bj-imdiridlem  38213  wl-axc11rc11  38622  poimirlem25  38670  axc11nfromc11  40090  aev-o  40095  oppcendc  50239