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 210	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  equcomd  2026  dvelimhw  2353  sb8v  2361  sb8f  2362  nfeqf1  2387  eu1  2614  reu7  3673  reu8  3674  dfdif3OLD  4049  issn  4763  disjxun  5070  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  dfid4  5514  dfid3  5516  opeliunxp  5685  opeliun2xp  5686  dmi  5863  elidinxp  5996  opabresid  6002  asymref2  6067  intirr  6068  cnvi  6092  coi1  6214  cnvso  6239  iotaval2  6456  brprcneu  6817  brprcneuALT  6818  dffv2  6922  fvn0ssdmfun  7015  f1oiso  7295  fvmpopr2d  7518  fsplit  8056  poxp2  8083  poxp3  8090  qsid  8718  mapsnend  8973  marypha2lem2  9339  fiinfg  9404  dfac5lem2  10037  dfac5lem3  10038  kmlem15  10078  brdom7disj  10444  suplem2pr  10967  wloglei  11673  fimaxre  12091  arch  12425  dflt2  13090  hashgt12el  14375  hashge2el2dif  14433  summo  15670  tosso  18374  opsrtoslem1  22031  mamulid  22424  mpomatmul  22429  mattpos1  22439  scmatscm  22496  1marepvmarrepid  22558  ist1-3  23332  unisngl  23510  fmid  23943  tgphaus  24100  dscopn  24556  iundisj2  25534  dvlip  25978  ply1divmo  26119  addsrid  27974  mulsrid  28123  disjabrex  32671  disjabrexf  32672  iundisj2f  32679  iundisj2fi  32889  grplsm0l  33486  esplyfvaln  33758  ordtconnlem1  34108  dfdm5  36001  dfrn5  36002  dffun10  36140  elfuns  36141  dfiota3  36149  brimg  36163  dfrdg4  36179  nn0prpwlem  36550  bj-axseprep  37427  fvineqsneu  37773  wl-equsalcom  37914  wl-sb9v  37920  matunitlindflem2  37984  ref5  38686  dfsucmap3  38830  pmapglb  40262  polval2N  40398  diclspsn  41686  sn-iotalem  42708  eq0rabdioph  43225  ontric3g  43966  undmrnresiss  44048  relopabVD  45344  icheq  47937  ichexmpl1  47944  pgnbgreunbgrlem4  48610  itsclquadeu  49268  oppcendc  49508