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  2349  sb8v  2357  sb8f  2358  nfeqf1  2383  eu1  2610  reu7  3678  reu8  3679  dfdif3OLD  4058  issn  4775  disjxun  5083  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  dfid4  5527  dfid3  5529  opeliunxp  5698  opeliun2xp  5699  dmi  5876  elidinxp  6009  opabresid  6015  asymref2  6080  intirr  6081  cnvi  6105  coi1  6227  cnvso  6252  iotaval2  6469  brprcneu  6830  brprcneuALT  6831  dffv2  6935  fvn0ssdmfun  7026  f1oiso  7306  fvmpopr2d  7529  fsplit  8067  poxp2  8093  poxp3  8100  qsid  8728  mapsnend  8983  marypha2lem2  9349  fiinfg  9414  dfac5lem2  10046  dfac5lem3  10047  kmlem15  10087  brdom7disj  10453  suplem2pr  10976  wloglei  11682  fimaxre  12100  arch  12434  dflt2  13099  hashgt12el  14384  hashge2el2dif  14442  summo  15679  tosso  18383  opsrtoslem1  22033  mamulid  22406  mpomatmul  22411  mattpos1  22421  scmatscm  22478  1marepvmarrepid  22540  ist1-3  23314  unisngl  23492  fmid  23925  tgphaus  24082  dscopn  24538  iundisj2  25516  dvlip  25960  ply1divmo  26101  addsrid  27956  mulsrid  28105  disjabrex  32652  disjabrexf  32653  iundisj2f  32660  iundisj2fi  32870  grplsm0l  33463  esplyfvaln  33718  ordtconnlem1  34068  dfdm5  35955  dfrn5  35956  dffun10  36094  elfuns  36095  dfiota3  36103  brimg  36117  dfrdg4  36133  nn0prpwlem  36504  bj-axseprep  37381  fvineqsneu  37727  wl-equsalcom  37868  wl-sb9v  37874  matunitlindflem2  37938  ref5  38640  dfsucmap3  38784  pmapglb  40216  polval2N  40352  diclspsn  41640  sn-iotalem  42662  eq0rabdioph  43208  ontric3g  43949  undmrnresiss  44031  relopabVD  45327  icheq  47922  ichexmpl1  47929  pgnbgreunbgrlem4  48595  itsclquadeu  49253  oppcendc  49493