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  3692  reu8  3693  dfdif3OLD  4069  issn  4783  iunidOLD  5010  disjxun  5090  copsexgw  5433  copsexg  5434  dfid4  5515  dfid3  5517  opeliunxp  5686  opeliun2xp  5687  dmi  5864  elidinxp  5995  opabresid  6001  asymref2  6066  intirr  6067  cnvi  6090  coi1  6211  cnvso  6236  iotaval2  6453  brprcneu  6812  brprcneuALT  6813  dffv2  6918  fvn0ssdmfun  7008  f1oiso  7288  fvmpopr2d  7511  fsplit  8050  poxp2  8076  poxp3  8083  qsid  8708  mapsnend  8961  marypha2lem2  9326  fiinfg  9391  dfac5lem2  10018  dfac5lem3  10019  kmlem15  10059  brdom7disj  10425  suplem2pr  10947  wloglei  11652  fimaxre  12069  arch  12381  dflt2  13050  hashgt12el  14329  hashge2el2dif  14387  summo  15624  tosso  18323  opsrtoslem1  21960  mamulid  22326  mpomatmul  22331  mattpos1  22341  scmatscm  22398  1marepvmarrepid  22460  ist1-3  23234  unisngl  23412  fmid  23845  tgphaus  24002  dscopn  24459  iundisj2  25448  dvlip  25896  ply1divmo  26039  addsrid  27876  mulsrid  28021  disjabrex  32526  disjabrexf  32527  iundisj2f  32534  iundisj2fi  32740  grplsm0l  33340  ordtconnlem1  33891  dfdm5  35750  dfrn5  35751  dffun10  35892  elfuns  35893  dfiota3  35901  brimg  35915  dfrdg4  35929  nn0prpwlem  36300  fvineqsneu  37389  wl-equsalcom  37521  wl-sb9v  37527  matunitlindflem2  37601  ref5  38291  pmapglb  39753  polval2N  39889  diclspsn  41177  sn-iotalem  42198  eq0rabdioph  42753  ontric3g  43499  undmrnresiss  43581  relopabVD  44878  icheq  47450  ichexmpl1  47457  pgnbgreunbgrlem4  48107  itsclquadeu  48766  oppcendc  49007