Theorem equcom 2048

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

Syntax hints:   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  equcomd  2049  dvelimhw  2377  sb8v  2385  sb8f  2386  nfeqf1  2411  eu1  2638  reu7  3695  reu8  3696  dfdif3OLD  4073  issn  4797  disjxun  5107  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  dfid4  5557  dfid3  5559  opeliunxp  5728  opeliun2xp  5729  cnvi  5871  dmi  5911  elidinxp  6046  opabresid  6052  asymref2  6117  intirr  6118  coi1  6264  cnvso  6289  iotaval2  6507  brprcneu  6871  brprcneuALT  6872  dffv2  6976  fvn0ssdmfun  7069  f1oiso  7349  fvmpopr2d  7572  fsplit  8108  poxp2  8135  poxp3  8142  qsid  8775  mapsnend  9029  marypha2lem2  9392  fiinfg  9457  dfac5lem2  10104  dfac5lem3  10105  kmlem15  10144  brdom7disj  10510  suplem2pr  11033  wloglei  11741  fimaxre  12154  arch  12496  dflt2  13168  hashgt12el  14455  hashge2el2dif  14513  summo  15764  tosso  18468  opsrtoslem1  22206  mamulid  22598  mpomatmul  22603  mattpos1  22613  scmatscm  22670  1marepvmarrepid  22732  ist1-3  23506  unisngl  23684  fmid  24117  tgphaus  24274  dscopn  24730  iundisj2  25708  dvlip  26152  ply1divmo  26293  addsrid  28157  mulsrid  28306  disjabrex  32927  disjabrexf  32928  iundisj2f  32935  iundisj2fi  33142  grplsm0l  33712  esplyfvaln  33964  ordtconnlem1  34314  dfdm5  36265  dfrn5  36266  dffun10  36404  elfuns  36405  dfiota3  36413  brimg  36427  dfrdg4  36443  nn0prpwlem  36853  bj-axseprep  37731  fvineqsneu  38077  wl-equsalcom  38218  wl-sb9v  38224  matunitlindflem2  38288  ref5  38988  dfsucmap3  39132  pmapglb  40564  polval2N  40700  diclspsn  41988  sn-iotalem  43012  eq0rabdioph  43527  ontric3g  44268  undmrnresiss  44350  relopabVD  45629  icheq  48231  ichexmpl1  48238  pgnbgreunbgrlem4  48904  itsclquadeu  49577  oppcendc  49816