Theorem equcom 2025

Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)

Assertion

Ref	Expression
equcom	⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 2024	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2024	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 211	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781

This theorem is referenced by:  equcomd  2026  equsb3rOLD  2111  dvelimhw  2366  nfeqf1  2397  eu1  2694  reu7  3725  reu8  3726  dfdif3  4093  issn  4765  iunid  4986  disjxun  5066  copsexgw  5383  copsexg  5384  opelopabsbALT  5418  dfid4  5463  dfid3  5464  opeliunxp  5621  dmi  5793  elidinxp  5913  opabresid  5919  opabresidOLD  5921  asymref2  5979  intirr  5980  cnvi  6002  coi1  6117  cnvso  6141  iotaval  6331  brprcneu  6664  dffv2  6758  fvn0ssdmfun  6844  f1oiso  7106  fsplit  7814  qsid  8365  mapsnend  8590  marypha2lem2  8902  fiinfg  8965  dfac5lem2  9552  dfac5lem3  9553  kmlem15  9592  brdom7disj  9955  suplem2pr  10477  wloglei  11174  fimaxre  11586  fimaxreOLD  11587  arch  11897  dflt2  12544  hashgt12el  13786  hashge2el2dif  13841  summo  15076  tosso  17648  opsrtoslem1  20266  mamulid  21052  mpomatmul  21057  mattpos1  21067  scmatscm  21124  1marepvmarrepid  21186  ist1-3  21959  unisngl  22137  fmid  22570  tgphaus  22727  dscopn  23185  iundisj2  24152  dvlip  24592  ply1divmo  24731  disjabrex  30334  disjabrexf  30335  iundisj2f  30342  iundisj2fi  30522  ordtconnlem1  31169  dfdm5  33018  dfrn5  33019  dffun10  33377  elfuns  33378  dfiota3  33386  brimg  33400  dfrdg4  33414  nn0prpwlem  33672  fvineqsneu  34694  wl-equsalcom  34784  wl-dfralflem  34840  matunitlindflem2  34891  pmapglb  36908  polval2N  37044  diclspsn  38332  eq0rabdioph  39380  ontric3g  39895  undmrnresiss  39971  relopabVD  41242  icheq  43627  ichexmpl1  43638  opeliun2xp  44388  itsclquadeu  44771