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

Theorem equid 1684
Description: Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Feb-2018.)
Assertion
Ref Expression
equid  |-  x  =  x

Proof of Theorem equid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 a9ev 1664 . . 3  |-  E. y 
y  =  x
2 ax-8 1683 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 45 . . 3  |-  ( y  =  x  ->  x  =  x )
41, 3eximii 1584 . 2  |-  E. y  x  =  x
5 ax17e 1625 . 2  |-  ( E. y  x  =  x  ->  x  =  x )
64, 5ax-mp 8 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   E.wex 1547
This theorem is referenced by:  nfequid  1686  equcomi  1687  stdpc6  1695  19.2OLD  1709  ax9dgen  1727  ax12dgen1  1736  ax12dgen3  1738  sbid  1943  equveliOLD  2043  ax11eq  2243  exists1  2343  vjust  2917  vex  2919  reu6  3083  nfccdeq  3119  sbc8g  3128  dfnul3  3591  rab0  3608  int0  4024  dfid3  4459  isso2i  4495  reusv5OLD  4692  reusv7OLD  4694  relop  4982  f1eqcocnv  5987  fsplit  6410  mpt2xopoveq  6429  ruv  7524  dfac2  7967  konigthlem  8399  hash2prde  11643  pospo  14385  alexsubALTlem3  18033  trust  18212  isppw2  20851  nbgranself  21399  usgrasscusgra  21445  avril1  21710  mathbox  23898  foo3  23899  domep  25363  dffix2  25659  mamulid  27326  elnev  27506  ipo0  27519  ifr0  27520  tratrb  28331  tratrbVD  28682  equveliNEW7  29232
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