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  2015  cbv2h  2036  equvini  2043  equviniOLD  2044  equveliOLD  2046  equsb2  2088  ax16i  2099  aecom-o  2205  ax10from10o  2231  aev-o  2236  axsep  4293  rext  4376  iotaval  5392  soxp  6422  axextnd  8426  prodmo  25219  finminlem  26215  dvelimhwNEW7  29165  ax10NEW7  29183  cbv2hwAUX7  29223  equviniNEW7  29235  equveliNEW7  29236  equsb2NEW7  29247  a16gNEW7  29254  ax16iNEW7  29259  ax7w3AUX7  29355  ax7w9AUX7  29364  alcomw9bAUX7  29365  cbv2hOLD7  29409
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