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  2284  cbv2w  2366  cbv2  2432  cbv2h  2435  axc16i  2465  equvini  2484  equsb2  2521  axsepgfromrep  5249  rext  5423  dfid2  5552  soxp  8127  xpord3inddlem  8152  axextnd  10600  prodmo  16023  mpomatmul  22668  cbvex1v  35583  finminlem  36937  bj-ssbid2ALT  37393  axc11n11  37415  axc11n11r  37416  bj-nnf-cbval  37513  bj-cbv2hv  37540  ax6er  37576  bj-dfid2ALT  37809  bj-imdiridlem  37937  wl-axc11rc11  38346  poimirlem25  38394  axc11nfromc11  39799  aev-o  39804  oppcendc  49944