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

Theorem equcom 1647
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 1646 . 2  |-  ( x  =  y  ->  y  =  x )
2 equcomi 1646 . 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  1649  ax12olem6  1873  eu1  2164  2eu6  2228  reu8  2961  iunid  3957  copsexg  4252  opelopabsbOLD  4273  dfid3  4310  relop  4834  dmi  4893  opabresid  5003  asymref2  5060  cnvi  5085  coi1  5188  cnvso  5214  brprcneu  5518  dffv2  5592  qsid  6725  mapsnen  6938  marypha2lem2  7189  dfac5lem2  7751  dfac5lem3  7752  brdom7disj  8156  suplem2pr  8677  fimaxre  9701  summo  12190  tosso  14142  ist1-3  17077  cnmptid  17355  fmid  17655  tgphaus  17799  dscopn  18096  dvlip  19340  disjabrex  23359  disjabrexf  23360  ghomf1olem  24001  dfdm5  24132  dfrn5  24133  dffun10  24453  elfuns  24454  dfiota3  24462  brimg  24476  dfrdg4  24488  restidsing  25076  mnlmxl2  25269  nn0prpwlem  26238  eq0rabdioph  26856  relopabVD  28677  ax12-4  29106  a12lem2  29131  pmapglb  29959  polval2N  30095  diclspsn  31384
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator