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

Theorem equcomi 1647
Description: Commutative law for equality. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 9-Apr-2017.)
Assertion
Ref Expression
equcomi  |-  ( x  =  y  ->  y  =  x )

Proof of Theorem equcomi
StepHypRef Expression
1 equid 1645 . 2  |-  x  =  x
2 ax-8 1644 . 2  |-  ( x  =  y  ->  (
x  =  x  -> 
y  =  x ) )
31, 2mpi 16 1  |-  ( x  =  y  ->  y  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equcom  1648  equequ1  1649  equcoms  1652  ax12dgen2  1701  sp  1717  dvelimfALT2  1737  ax12olem1  1870  ax10  1886  a16gALT  1887  cbv2h  1923  equvini  1930  equveli  1931  aev  1934  ax16i  1942  equsb2  1980  alequcom-o  2092  ax10from10o  2118  aev-o  2123  axsep  4141  rext  4221  soxp  6190  iotaval  6264  axextnd  8209  inpc  24688  finminlem  25642  hbae-x12  28388  a12stdy2-x12  28391  equvinv  28393  equvelv  28395  ax10lem18ALT  28403  a12study  28411  a12study3  28414  a12study10n  28416
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 1636  ax-8 1644
  Copyright terms: Public domain W3C validator