Theorem equcom 2019

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

Syntax hints:   ↔ wb 206

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 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  equcomd  2020  dvelimhw  2349  sb8v  2357  sb8f  2358  nfeqf1  2383  eu1  2610  reu7  3690  reu8  3691  dfdif3OLD  4070  issn  4788  disjxun  5096  copsexgw  5438  copsexg  5439  dfid4  5520  dfid3  5522  opeliunxp  5691  opeliun2xp  5692  dmi  5870  elidinxp  6003  opabresid  6009  asymref2  6074  intirr  6075  cnvi  6099  coi1  6221  cnvso  6246  iotaval2  6463  brprcneu  6824  brprcneuALT  6825  dffv2  6929  fvn0ssdmfun  7019  f1oiso  7297  fvmpopr2d  7520  fsplit  8059  poxp2  8085  poxp3  8092  qsid  8718  mapsnend  8973  marypha2lem2  9339  fiinfg  9404  dfac5lem2  10034  dfac5lem3  10035  kmlem15  10075  brdom7disj  10441  suplem2pr  10964  wloglei  11669  fimaxre  12086  arch  12398  dflt2  13062  hashgt12el  14345  hashge2el2dif  14403  summo  15640  tosso  18340  opsrtoslem1  22010  mamulid  22385  mpomatmul  22390  mattpos1  22400  scmatscm  22457  1marepvmarrepid  22519  ist1-3  23293  unisngl  23471  fmid  23904  tgphaus  24061  dscopn  24517  iundisj2  25506  dvlip  25954  ply1divmo  26097  addsrid  27960  mulsrid  28109  disjabrex  32657  disjabrexf  32658  iundisj2f  32665  iundisj2fi  32877  grplsm0l  33484  ordtconnlem1  34081  dfdm5  35967  dfrn5  35968  dffun10  36106  elfuns  36107  dfiota3  36115  brimg  36129  dfrdg4  36145  nn0prpwlem  36516  bj-df-sb  36853  fvineqsneu  37616  wl-equsalcom  37748  wl-sb9v  37754  matunitlindflem2  37818  ref5  38514  dfsucmap3  38647  pmapglb  40040  polval2N  40176  diclspsn  41464  sn-iotalem  42487  eq0rabdioph  43028  ontric3g  43773  undmrnresiss  43855  relopabVD  45151  icheq  47718  ichexmpl1  47725  pgnbgreunbgrlem4  48375  itsclquadeu  49033  oppcendc  49273