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  2176  sbequ2  2287  cbv2w  2371  cbv2  2437  cbv2h  2440  axc16i  2470  equvini  2489  equsb2  2526  axsepgfromrep  5257  rext  5431  dfid2  5560  soxp  8127  xpord3inddlem  8152  axextnd  10587  prodmo  16009  mpomatmul  22633  cbvex1v  35503  finminlem  36862  bj-ssbid2ALT  37318  axc11n11  37340  axc11n11r  37341  bj-nnf-cbval  37438  bj-cbv2hv  37465  ax6er  37501  bj-dfid2ALT  37734  bj-imdiridlem  37862  wl-axc11rc11  38271  poimirlem25  38329  axc11nfromc11  39733  aev-o  39738  oppcendc  49829