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

Theorem equcom 1671
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 1670 . 2  |-  ( x  =  y  ->  y  =  x )
2 equcomi 1670 . 2  |-  ( y  =  x  ->  x  =  y )
31, 2impbii 180 1  |-  ( x  =  y  <->  y  =  x )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  equequ2  1677  ax12olem6  1904  eu1  2197  2eu6  2261  reu8  2995  iunid  3994  copsexg  4289  opelopabsbOLD  4310  dfid3  4347  relop  4871  dmi  4930  opabresid  5040  asymref2  5097  cnvi  5122  coi1  5225  cnvso  5251  brprcneu  5556  dffv2  5630  qsid  6767  mapsnen  6981  marypha2lem2  7234  dfac5lem2  7796  dfac5lem3  7797  brdom7disj  8201  suplem2pr  8722  fimaxre  9746  summo  12237  tosso  14191  ist1-3  17133  cnmptid  17411  fmid  17707  tgphaus  17851  dscopn  18148  dvlip  19393  disjabrex  23167  disjabrexf  23168  ghomf1olem  24285  dfid4  24364  dfdm5  24517  dfrn5  24518  dffun10  24838  elfuns  24839  dfiota3  24847  brimg  24861  dfrdg4  24874  nn0prpwlem  25387  eq0rabdioph  26004  hashgt12el  27280  relopabVD  28188  ax12olem6NEW7  28631  ax12-4  28924  a12lem2  28949  pmapglb  29777  polval2N  29913  diclspsn  31202
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666
This theorem depends on definitions:  df-bi 177  df-ex 1533
  Copyright terms: Public domain W3C validator