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

Theorem equid 1840
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.) (Proof shortened by Wolf Lammen, 22-Aug-2020.)
Assertion
Ref Expression
equid  |-  x  =  x

Proof of Theorem equid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ax6ev 1796 . 2  |-  E. y 
y  =  x
2 ax-7 1839 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 49 . . 3  |-  ( y  =  x  ->  x  =  x )
43exlimiv 1766 . 2  |-  ( E. y  y  =  x  ->  x  =  x )
51, 4ax-mp 5 1  |-  x  =  x
Colors of variables: wff setvar class
Syntax hints:   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  nfequid  1842  equcomi  1843  stdpc6  1850  ax6dgen  1874  ax13dgen1  1883  ax13dgen3  1885  sbid  2050  exists1  2359  vjust  3082  vex  3084  reu6  3260  nfccdeq  3297  sbc8g  3307  dfnul3  3764  rab0  3783  int0  4266  dfid3  4766  isso2i  4803  relop  5001  f1eqcocnv  6211  fsplit  6909  mpt2xopoveq  6970  ruv  8118  dfac2  8562  konigthlem  8994  hash2prde  12629  hashge2el2difr  12635  pospo  16207  mamulid  19453  mdetdiagid  19612  alexsubALTlem3  21051  trust  21231  isppw2  24029  xmstrkgc  24903  nbgranself  25148  usgrasscusgra  25197  rusgrasn  25659  avril1  25886  mathbox  28081  foo3  28082  domep  30434  wlimeq12  30497  bj-vjust  31359  mptsnunlem  31681  ax12eq  32431  elnev  36647  ipo0  36660  ifr0  36661  tratrb  36755  tratrbVD  37119
  Copyright terms: Public domain W3C validator