MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equcom Structured version   Unicode version

Theorem equcom 1692
Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom  |-  ( x  =  y  <->  y  =  x )

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1691 . 2  |-  ( x  =  y  ->  y  =  x )
2 equcomi 1691 . 2  |-  ( y  =  x  ->  x  =  y )
31, 2impbii 181 1  |-  ( x  =  y  <->  y  =  x )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  equequ2  1698  dvelimhw  1876  ax12olem6OLD  2016  eu1  2302  2eu6  2366  reu7  3129  reu8  3130  iunid  4146  disjxun  4210  copsexg  4442  opelopabsbOLD  4463  dfid3  4499  opeliunxp  4929  relop  5023  dmi  5084  opabresid  5194  asymref2  5251  intirr  5252  cnvi  5276  coi1  5385  cnvso  5411  brprcneu  5721  dffv2  5796  f1oiso  6071  qsid  6970  mapsnen  7184  marypha2lem2  7441  dfac5lem2  8005  dfac5lem3  8006  kmlem15  8044  brdom7disj  8409  suplem2pr  8930  wloglei  9559  fimaxre  9955  arch  10218  dflt2  10741  hashgt12el  11682  summo  12511  tosso  14465  opsrtoslem1  16544  ist1-3  17413  cnmptid  17693  fmid  17992  tgphaus  18146  dscopn  18621  iundisj2  19443  dvlip  19877  ply1divmo  20058  disjabrex  24024  disjabrexf  24025  iundisj2f  24030  iundisj2fi  24153  ghomf1olem  25105  dfid4  25183  dfdm5  25400  dfrn5  25401  dffun10  25759  elfuns  25760  dfiota3  25768  brimg  25782  dfrdg4  25795  nn0prpwlem  26325  eq0rabdioph  26835  frg2wot1  28446  relopabVD  29013  ax12olem6NEW7  29459  pmapglb  30567  polval2N  30703  diclspsn  31992
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator