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

Theorem equcomi 1679
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 1676 . 2  |-  x  =  x
2 ax-8 1675 . 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  1680  equcoms  1681  equequ1OLD  1685  ax12dgen2  1726  spOLD  1749  dvelimhw  1854  ax12olem1  1932  ax10  1949  a16g  1950  cbv2h  1985  equvini  1992  equveli  1993  equsb2  2040  ax16i  2051  aecom-o  2156  ax10from10o  2182  aev-o  2187  axsep  4221  rext  4304  iotaval  5312  soxp  6315  axextnd  8303  prodmo  24563  finminlem  25555  dvelimhwNEW7  28878  ax10NEW7  28896  cbv2hwAUX7  28936  equviniNEW7  28948  equveliNEW7  28949  equsb2NEW7  28960  a16gNEW7  28967  ax16iNEW7  28972  ax7w3AUX7  29068  ax7w9AUX7  29077  alcomw9bAUX7  29078  cbv2hOLD7  29122  hbae-x12  29178  a12stdy2-x12  29181  equvinv  29183  equvelv  29185  ax10lem18ALT  29193  a12study  29201  a12study3  29204  a12study10n  29206
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator