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

Syntax hints:   ↔ wb 209

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  equcomd  2026  equsb3rOLD  2108  dvelimhw  2355  nfeqf1  2386  eu1  2630  reu7  3648  reu8  3649  dfdif3  4022  issn  4723  iunid  4952  disjxun  5033  copsexgw  5352  copsexg  5353  dfid4  5434  dfid3  5435  opeliunxp  5592  dmi  5766  elidinxp  5887  opabresid  5893  opabresidOLD  5895  asymref2  5953  intirr  5954  cnvi  5976  coi1  6096  cnvso  6121  iotaval  6313  brprcneu  6653  fvprc  6654  dffv2  6751  fvn0ssdmfun  6838  f1oiso  7103  fvmpopr2d  7311  fsplit  7822  qsid  8378  mapsnend  8612  marypha2lem2  8938  fiinfg  9001  dfac5lem2  9589  dfac5lem3  9590  kmlem15  9629  brdom7disj  9996  suplem2pr  10518  wloglei  11215  fimaxre  11627  arch  11936  dflt2  12587  hashgt12el  13838  hashge2el2dif  13895  summo  15127  tosso  17717  opsrtoslem1  20820  mamulid  21146  mpomatmul  21151  mattpos1  21161  scmatscm  21218  1marepvmarrepid  21280  ist1-3  22054  unisngl  22232  fmid  22665  tgphaus  22822  dscopn  23280  iundisj2  24254  dvlip  24697  ply1divmo  24840  disjabrex  30448  disjabrexf  30449  iundisj2f  30456  iundisj2fi  30646  grplsm0l  31116  ordtconnlem1  31399  dfdm5  33267  dfrn5  33268  poxp2  33349  poxp3  33355  xpord3ind  33359  addsid1  33702  dffun10  33791  elfuns  33792  dfiota3  33800  brimg  33814  dfrdg4  33828  nn0prpwlem  34086  fvineqsneu  35134  wl-equsalcom  35253  wl-dfralflem  35309  matunitlindflem2  35360  pmapglb  37372  polval2N  37508  diclspsn  38796  eq0rabdioph  40118  ontric3g  40631  undmrnresiss  40705  relopabVD  42008  icheq  44375  ichexmpl1  44382  opeliun2xp  45129  itsclquadeu  45584