Theorem equcom 2050

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  equcomd  2051  dvelimhw  2374  sb8v  2382  sb8f  2383  nfeqf1  2408  eu1  2635  reu7  3689  reu8  3690  issn  4786  disjxun  5100  copsexgwOLD  5461  dfid4  5547  dfid3  5549  opeliunxp  5718  opeliun2xp  5719  cnvi  5864  dmi  5904  elidinxp  6038  opabresid  6044  asymref2  6113  intirr  6114  coi1  6267  cnvso  6294  iotaval2  6512  brprcneu  6880  brprcneuALT  6881  dffv2  6985  fvn0ssdmfun  7079  f1oiso  7363  fvmpopr2d  7586  fsplit  8135  poxp2  8167  poxp3  8174  qsid  8810  mapsnend  9072  marypha2lem2  9435  fiinfg  9500  dfac5lem2  10210  dfac5lem3  10211  kmlem15  10250  brdom7disj  10617  suplem2pr  11145  wloglei  11855  fimaxre  12268  arch  12610  dflt2  13284  hashgt12el  14574  hashge2el2dif  14632  summo  15892  tosso  18600  opsrtoslem1  22373  mamulid  22765  mpomatmul  22770  mattpos1  22780  scmatscm  22837  1marepvmarrepid  22899  matunitlindflem2  23004  ist1-3  23676  unisngl  23855  fmid  24288  tgphaus  24445  dscopn  24901  iundisj2  25879  dvlip  26322  ply1divmo  26463  addsrid  28359  mulsrid  28508  disjabrex  33227  disjabrexf  33228  iundisj2f  33235  iundisj2fi  33439  grplsm0l  34004  esplyfvaln  34256  ordtconnlem1  34606  dfdm5  36661  dfrn5  36662  dffun10  36800  elfuns  36801  dfiota3  36809  brimg  36823  dfrdg4  36839  nn0prpwlem  37234  coi1res  38096  bj-axseprep  38126  fvineqsneu  38471  wl-equsalcom  38612  wl-sb9v  38618  ref5  39388  dfsucmap3  39532  pmapglb  40964  polval2N  41100  diclspsn  42388  sn-iotalem  43412  eq0rabdioph  43924  ontric3g  44660  undmrnresiss  44741  relopabVD  46019  icheq  48680  ichexmpl1  48687  pgnbgreunbgrlem4  49353  itsclquadeu  50025  oppcendc  50268