Theorem equcom 2019

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 2018	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2018	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  equcomd  2020  dvelimhw  2347  sb8v  2355  sb8f  2356  nfeqf1  2381  eu1  2608  reu7  3688  reu8  3689  dfdif3OLD  4068  issn  4786  disjxun  5094  copsexgw  5436  copsexg  5437  dfid4  5518  dfid3  5520  opeliunxp  5689  opeliun2xp  5690  dmi  5868  elidinxp  6001  opabresid  6007  asymref2  6072  intirr  6073  cnvi  6097  coi1  6219  cnvso  6244  iotaval2  6461  brprcneu  6822  brprcneuALT  6823  dffv2  6927  fvn0ssdmfun  7017  f1oiso  7295  fvmpopr2d  7518  fsplit  8057  poxp2  8083  poxp3  8090  qsid  8716  mapsnend  8971  marypha2lem2  9337  fiinfg  9402  dfac5lem2  10032  dfac5lem3  10033  kmlem15  10073  brdom7disj  10439  suplem2pr  10962  wloglei  11667  fimaxre  12084  arch  12396  dflt2  13060  hashgt12el  14343  hashge2el2dif  14401  summo  15638  tosso  18338  opsrtoslem1  22008  mamulid  22383  mpomatmul  22388  mattpos1  22398  scmatscm  22455  1marepvmarrepid  22517  ist1-3  23291  unisngl  23469  fmid  23902  tgphaus  24059  dscopn  24515  iundisj2  25504  dvlip  25952  ply1divmo  26095  addsrid  27934  mulsrid  28082  disjabrex  32606  disjabrexf  32607  iundisj2f  32614  iundisj2fi  32826  grplsm0l  33433  ordtconnlem1  34030  dfdm5  35916  dfrn5  35917  dffun10  36055  elfuns  36056  dfiota3  36064  brimg  36078  dfrdg4  36094  nn0prpwlem  36465  bj-df-sb  36796  fvineqsneu  37555  wl-equsalcom  37687  wl-sb9v  37693  matunitlindflem2  37757  ref5  38451  dfsucmap3  38576  pmapglb  39969  polval2N  40105  diclspsn  41393  sn-iotalem  42419  eq0rabdioph  42960  ontric3g  43705  undmrnresiss  43787  relopabVD  45083  icheq  47650  ichexmpl1  47657  pgnbgreunbgrlem4  48307  itsclquadeu  48965  oppcendc  49205