Theorem equcom 2022

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 2021	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2021	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 208	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  equcomd  2023  dvelimhw  2342  sb8v  2349  sb8f  2350  nfeqf1  2379  eu1  2607  reu7  3727  reu8  3728  dfdif3  4113  issn  4832  iunidOLD  5063  disjxun  5145  copsexgw  5489  copsexg  5490  dfid4  5574  dfid3  5576  opeliunxp  5741  dmi  5919  elidinxp  6041  opabresid  6047  asymref2  6115  intirr  6116  cnvi  6138  coi1  6258  cnvso  6284  iotaval2  6508  iotavalOLD  6514  brprcneu  6878  brprcneuALT  6879  dffv2  6982  fvn0ssdmfun  7072  f1oiso  7343  fvmpopr2d  7564  fsplit  8098  poxp2  8124  poxp3  8131  qsid  8773  mapsnend  9032  marypha2lem2  9427  fiinfg  9490  dfac5lem2  10115  dfac5lem3  10116  kmlem15  10155  brdom7disj  10522  suplem2pr  11044  wloglei  11742  fimaxre  12154  arch  12465  dflt2  13123  hashgt12el  14378  hashge2el2dif  14437  summo  15659  tosso  18368  opsrtoslem1  21598  mamulid  21925  mpomatmul  21930  mattpos1  21940  scmatscm  21997  1marepvmarrepid  22059  ist1-3  22835  unisngl  23013  fmid  23446  tgphaus  23603  dscopn  24064  iundisj2  25048  dvlip  25492  ply1divmo  25635  addsrid  27428  mulsrid  27549  disjabrex  31791  disjabrexf  31792  iundisj2f  31799  iundisj2fi  31986  grplsm0l  32478  ordtconnlem1  32842  dfdm5  34682  dfrn5  34683  dffun10  34824  elfuns  34825  dfiota3  34833  brimg  34847  dfrdg4  34861  nn0prpwlem  35145  fvineqsneu  36230  wl-equsalcom  36349  matunitlindflem2  36423  ref5  37120  pmapglb  38579  polval2N  38715  diclspsn  40003  sn-iotalem  40986  eq0rabdioph  41447  ontric3g  42206  undmrnresiss  42288  relopabVD  43595  icheq  46065  ichexmpl1  46072  opeliun2xp  46910  itsclquadeu  47365