Theorem equcom 2020

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 2019	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2019	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  equcomd  2021  dvelimhw  2350  sb8v  2358  sb8f  2359  nfeqf1  2384  eu1  2611  reu7  3692  reu8  3693  dfdif3OLD  4072  issn  4790  disjxun  5098  copsexgw  5446  copsexg  5447  dfid4  5528  dfid3  5530  opeliunxp  5699  opeliun2xp  5700  dmi  5878  elidinxp  6011  opabresid  6017  asymref2  6082  intirr  6083  cnvi  6107  coi1  6229  cnvso  6254  iotaval2  6471  brprcneu  6832  brprcneuALT  6833  dffv2  6937  fvn0ssdmfun  7028  f1oiso  7307  fvmpopr2d  7530  fsplit  8069  poxp2  8095  poxp3  8102  qsid  8730  mapsnend  8985  marypha2lem2  9351  fiinfg  9416  dfac5lem2  10046  dfac5lem3  10047  kmlem15  10087  brdom7disj  10453  suplem2pr  10976  wloglei  11681  fimaxre  12098  arch  12410  dflt2  13074  hashgt12el  14357  hashge2el2dif  14415  summo  15652  tosso  18352  opsrtoslem1  22022  mamulid  22397  mpomatmul  22402  mattpos1  22412  scmatscm  22469  1marepvmarrepid  22531  ist1-3  23305  unisngl  23483  fmid  23916  tgphaus  24073  dscopn  24529  iundisj2  25518  dvlip  25966  ply1divmo  26109  addsrid  27972  mulsrid  28121  disjabrex  32669  disjabrexf  32670  iundisj2f  32677  iundisj2fi  32888  grplsm0l  33496  esplyfvaln  33751  ordtconnlem1  34102  dfdm5  35989  dfrn5  35990  dffun10  36128  elfuns  36129  dfiota3  36137  brimg  36151  dfrdg4  36167  nn0prpwlem  36538  bj-df-sb  36897  bj-axseprep  37322  fvineqsneu  37666  wl-equsalcom  37798  wl-sb9v  37804  matunitlindflem2  37868  ref5  38570  dfsucmap3  38714  pmapglb  40146  polval2N  40282  diclspsn  41570  sn-iotalem  42593  eq0rabdioph  43133  ontric3g  43878  undmrnresiss  43960  relopabVD  45256  icheq  47822  ichexmpl1  47829  pgnbgreunbgrlem4  48479  itsclquadeu  49137  oppcendc  49377