Theorem equcom 2020

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 2019	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2019	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  equcomd  2021  dvelimhw  2350  sb8v  2358  sb8f  2359  nfeqf1  2384  eu1  2611  reu7  3679  reu8  3680  dfdif3OLD  4059  issn  4776  disjxun  5084  copsexgw  5439  copsexg  5440  dfid4  5521  dfid3  5523  opeliunxp  5692  opeliun2xp  5693  dmi  5871  elidinxp  6004  opabresid  6010  asymref2  6075  intirr  6076  cnvi  6100  coi1  6222  cnvso  6247  iotaval2  6464  brprcneu  6825  brprcneuALT  6826  dffv2  6930  fvn0ssdmfun  7021  f1oiso  7300  fvmpopr2d  7523  fsplit  8061  poxp2  8087  poxp3  8094  qsid  8722  mapsnend  8977  marypha2lem2  9343  fiinfg  9408  dfac5lem2  10040  dfac5lem3  10041  kmlem15  10081  brdom7disj  10447  suplem2pr  10970  wloglei  11676  fimaxre  12094  arch  12428  dflt2  13093  hashgt12el  14378  hashge2el2dif  14436  summo  15673  tosso  18377  opsrtoslem1  22046  mamulid  22419  mpomatmul  22424  mattpos1  22434  scmatscm  22491  1marepvmarrepid  22553  ist1-3  23327  unisngl  23505  fmid  23938  tgphaus  24095  dscopn  24551  iundisj2  25529  dvlip  25973  ply1divmo  26114  addsrid  27973  mulsrid  28122  disjabrex  32670  disjabrexf  32671  iundisj2f  32678  iundisj2fi  32888  grplsm0l  33481  esplyfvaln  33736  ordtconnlem1  34087  dfdm5  35974  dfrn5  35975  dffun10  36113  elfuns  36114  dfiota3  36122  brimg  36136  dfrdg4  36152  nn0prpwlem  36523  bj-axseprep  37400  fvineqsneu  37744  wl-equsalcom  37885  wl-sb9v  37891  matunitlindflem2  37955  ref5  38657  dfsucmap3  38801  pmapglb  40233  polval2N  40369  diclspsn  41657  sn-iotalem  42679  eq0rabdioph  43225  ontric3g  43970  undmrnresiss  44052  relopabVD  45348  icheq  47937  ichexmpl1  47944  pgnbgreunbgrlem4  48610  itsclquadeu  49268  oppcendc  49508