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

Theorem equcomi 1687
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 1684 . 2  |-  x  =  x
2 ax-8 1683 . 2  |-  ( x  =  y  ->  (
x  =  x  -> 
y  =  x ) )
31, 2mpi 17 1  |-  ( x  =  y  ->  y  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equcom  1688  equcoms  1689  equequ1OLD  1693  ax12dgen2  1737  spOLD  1760  dvelimhwOLD  1873  ax12olem1  1972  ax12olem1OLD  1977  ax10  1991  ax10OLD  1998  a16gOLD  2013  cbv2h  2033  equvini  2040  equviniOLD  2041  equveliOLD  2043  equsb2  2084  ax16i  2095  aecom-o  2201  ax10from10o  2227  aev-o  2232  axsep  4289  rext  4372  iotaval  5388  soxp  6418  axextnd  8422  prodmo  25215  finminlem  26211  dvelimhwNEW7  29161  ax10NEW7  29179  cbv2hwAUX7  29219  equviniNEW7  29231  equveliNEW7  29232  equsb2NEW7  29243  a16gNEW7  29250  ax16iNEW7  29255  ax7w3AUX7  29351  ax7w9AUX7  29360  alcomw9bAUX7  29361  cbv2hOLD7  29405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator