Theorem equcom 2015

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 2014	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2014	. 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 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005

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

This theorem is referenced by:  equcomd  2016  dvelimhw  2346  sb8v  2353  sb8f  2354  nfeqf1  2382  eu1  2608  reu7  3741  reu8  3742  dfdif3OLD  4128  issn  4837  iunidOLD  5066  disjxun  5146  copsexgw  5501  copsexg  5502  dfid4  5584  dfid3  5586  opeliunxp  5756  dmi  5935  elidinxp  6064  opabresid  6070  asymref2  6140  intirr  6141  cnvi  6164  coi1  6284  cnvso  6310  iotaval2  6531  iotavalOLD  6537  brprcneu  6897  brprcneuALT  6898  dffv2  7004  fvn0ssdmfun  7094  f1oiso  7371  fvmpopr2d  7595  fsplit  8141  poxp2  8167  poxp3  8174  qsid  8822  mapsnend  9075  marypha2lem2  9474  fiinfg  9537  dfac5lem2  10162  dfac5lem3  10163  kmlem15  10203  brdom7disj  10569  suplem2pr  11091  wloglei  11793  fimaxre  12210  arch  12521  dflt2  13187  hashgt12el  14458  hashge2el2dif  14516  summo  15750  tosso  18477  opsrtoslem1  22097  mamulid  22463  mpomatmul  22468  mattpos1  22478  scmatscm  22535  1marepvmarrepid  22597  ist1-3  23373  unisngl  23551  fmid  23984  tgphaus  24141  dscopn  24602  iundisj2  25598  dvlip  26047  ply1divmo  26190  addsrid  28012  mulsrid  28154  disjabrex  32602  disjabrexf  32603  iundisj2f  32610  iundisj2fi  32805  grplsm0l  33411  ordtconnlem1  33885  dfdm5  35754  dfrn5  35755  dffun10  35896  elfuns  35897  dfiota3  35905  brimg  35919  dfrdg4  35933  nn0prpwlem  36305  fvineqsneu  37394  wl-equsalcom  37524  wl-sb9v  37530  matunitlindflem2  37604  ref5  38295  pmapglb  39753  polval2N  39889  diclspsn  41177  sn-iotalem  42239  eq0rabdioph  42764  ontric3g  43512  undmrnresiss  43594  relopabVD  44899  icheq  47387  ichexmpl1  47394  opeliun2xp  48178  itsclquadeu  48627