Theorem equcom 2016

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 2015	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2015	. 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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006

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

This theorem is referenced by:  equcomd  2017  dvelimhw  2346  sb8v  2354  sb8f  2355  nfeqf1  2383  eu1  2609  reu7  3737  reu8  3738  dfdif3OLD  4117  issn  4831  iunidOLD  5060  disjxun  5140  copsexgw  5494  copsexg  5495  dfid4  5578  dfid3  5580  opeliunxp  5751  opeliun2xp  5752  dmi  5931  elidinxp  6061  opabresid  6067  asymref2  6136  intirr  6137  cnvi  6160  coi1  6281  cnvso  6307  iotaval2  6528  iotavalOLD  6534  brprcneu  6895  brprcneuALT  6896  dffv2  7003  fvn0ssdmfun  7093  f1oiso  7372  fvmpopr2d  7596  fsplit  8143  poxp2  8169  poxp3  8176  qsid  8824  mapsnend  9077  marypha2lem2  9477  fiinfg  9540  dfac5lem2  10165  dfac5lem3  10166  kmlem15  10206  brdom7disj  10572  suplem2pr  11094  wloglei  11796  fimaxre  12213  arch  12525  dflt2  13191  hashgt12el  14462  hashge2el2dif  14520  summo  15754  tosso  18465  opsrtoslem1  22080  mamulid  22448  mpomatmul  22453  mattpos1  22463  scmatscm  22520  1marepvmarrepid  22582  ist1-3  23358  unisngl  23536  fmid  23969  tgphaus  24126  dscopn  24587  iundisj2  25585  dvlip  26033  ply1divmo  26176  addsrid  27998  mulsrid  28140  disjabrex  32596  disjabrexf  32597  iundisj2f  32604  iundisj2fi  32800  grplsm0l  33432  ordtconnlem1  33924  dfdm5  35774  dfrn5  35775  dffun10  35916  elfuns  35917  dfiota3  35925  brimg  35939  dfrdg4  35953  nn0prpwlem  36324  fvineqsneu  37413  wl-equsalcom  37545  wl-sb9v  37551  matunitlindflem2  37625  ref5  38315  pmapglb  39773  polval2N  39909  diclspsn  41197  sn-iotalem  42261  eq0rabdioph  42792  ontric3g  43540  undmrnresiss  43622  relopabVD  44926  icheq  47454  ichexmpl1  47461  itsclquadeu  48703  oppcendc  48921