Theorem equcomi 2052

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 2047	. 2 ⊢ 𝑥 = 𝑥
2		ax7 2051	. 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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  equcom  2053  equcoms  2055  ax13dgen2  2177  ax12ev2c  2220  sbequ2  2288  cbv2w  2370  cbv2  2435  cbv2h  2438  axc16i  2468  equvini  2487  equsb2  2524  axsepgfromrep  5253  rext  5423  dfid2  5555  soxp  8178  xpord3inddlem  8208  axextnd  10715  prodmo  16147  mpomatmul  22816  cbvex1v  35815  finminlem  37321  bj-ssbid2ALT  37777  axc11n11  37799  axc11n11r  37800  bj-nnf-cbval  37897  bj-cbv2hv  37924  ax6er  37960  bj-dfid2ALT  38250  bj-imdiridlem  38374  wl-axc11rc11  38783  poimirlem25  38831  axc11nfromc11  40249  aev-o  40254  oppcendc  50463