Theorem equcom 2018

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 2017	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2017	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  equcomd  2019  dvelimhw  2343  sb8v  2351  sb8f  2352  nfeqf1  2377  eu1  2603  reu7  3703  reu8  3704  dfdif3OLD  4081  issn  4796  iunidOLD  5025  disjxun  5105  copsexgw  5450  copsexg  5451  dfid4  5534  dfid3  5536  opeliunxp  5705  opeliun2xp  5706  dmi  5885  elidinxp  6015  opabresid  6021  asymref2  6090  intirr  6091  cnvi  6114  coi1  6235  cnvso  6261  iotaval2  6479  iotavalOLD  6485  brprcneu  6848  brprcneuALT  6849  dffv2  6956  fvn0ssdmfun  7046  f1oiso  7326  fvmpopr2d  7551  fsplit  8096  poxp2  8122  poxp3  8129  qsid  8754  mapsnend  9007  marypha2lem2  9387  fiinfg  9452  dfac5lem2  10077  dfac5lem3  10078  kmlem15  10118  brdom7disj  10484  suplem2pr  11006  wloglei  11710  fimaxre  12127  arch  12439  dflt2  13108  hashgt12el  14387  hashge2el2dif  14445  summo  15683  tosso  18378  opsrtoslem1  21962  mamulid  22328  mpomatmul  22333  mattpos1  22343  scmatscm  22400  1marepvmarrepid  22462  ist1-3  23236  unisngl  23414  fmid  23847  tgphaus  24004  dscopn  24461  iundisj2  25450  dvlip  25898  ply1divmo  26041  addsrid  27871  mulsrid  28016  disjabrex  32511  disjabrexf  32512  iundisj2f  32519  iundisj2fi  32720  grplsm0l  33374  ordtconnlem1  33914  dfdm5  35760  dfrn5  35761  dffun10  35902  elfuns  35903  dfiota3  35911  brimg  35925  dfrdg4  35939  nn0prpwlem  36310  fvineqsneu  37399  wl-equsalcom  37531  wl-sb9v  37537  matunitlindflem2  37611  ref5  38301  pmapglb  39764  polval2N  39900  diclspsn  41188  sn-iotalem  42209  eq0rabdioph  42764  ontric3g  43511  undmrnresiss  43593  relopabVD  44890  icheq  47463  ichexmpl1  47470  pgnbgreunbgrlem4  48109  itsclquadeu  48766  oppcendc  49007