Theorem equcom 2038

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 2037	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2037	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 211	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by:  equcomd  2039  dvelimhw  2376  sb8v  2384  sb8f  2385  nfeqf1  2410  eu1  2637  reu7  3695  reu8  3696  dfdif3OLD  4072  issn  4790  disjxun  5098  copsexgw  5458  copsexgwOLD  5459  copsexg  5460  dfid4  5543  dfid3  5545  opeliunxp  5714  opeliun2xp  5715  cnvi  5857  dmi  5897  elidinxp  6033  opabresid  6039  asymref2  6104  intirr  6105  coi1  6250  cnvso  6275  iotaval2  6492  brprcneu  6857  brprcneuALT  6858  dffv2  6962  fvn0ssdmfun  7055  f1oiso  7335  fvmpopr2d  7558  fsplit  8096  poxp2  8123  poxp3  8130  qsid  8763  mapsnend  9017  marypha2lem2  9382  fiinfg  9447  dfac5lem2  10080  dfac5lem3  10081  kmlem15  10121  brdom7disj  10488  suplem2pr  11011  wloglei  11719  fimaxre  12136  arch  12478  dflt2  13150  hashgt12el  14435  hashge2el2dif  14493  summo  15744  tosso  18449  opsrtoslem1  22108  mamulid  22501  mpomatmul  22506  mattpos1  22516  scmatscm  22573  1marepvmarrepid  22635  ist1-3  23409  unisngl  23587  fmid  24020  tgphaus  24177  dscopn  24633  iundisj2  25611  dvlip  26055  ply1divmo  26196  addsrid  28057  mulsrid  28206  disjabrex  32782  disjabrexf  32783  iundisj2f  32790  iundisj2fi  32999  grplsm0l  33589  esplyfvaln  33871  ordtconnlem1  34221  dfdm5  36123  dfrn5  36124  dffun10  36262  elfuns  36263  dfiota3  36271  brimg  36285  dfrdg4  36301  nn0prpwlem  36682  bj-axseprep  37559  fvineqsneu  37905  wl-equsalcom  38046  wl-sb9v  38052  matunitlindflem2  38116  ref5  38818  dfsucmap3  38962  pmapglb  40394  polval2N  40530  diclspsn  41818  sn-iotalem  42840  eq0rabdioph  43357  ontric3g  44098  undmrnresiss  44180  relopabVD  45476  icheq  48068  ichexmpl1  48075  pgnbgreunbgrlem4  48741  itsclquadeu  49399  oppcendc  49639