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

Theorem equid 1688
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 1668 . . 3  |-  E. y 
y  =  x
2 ax-8 1687 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 45 . . 3  |-  ( y  =  x  ->  x  =  x )
41, 3eximii 1587 . 2  |-  E. y  x  =  x
5 ax17e 1628 . 2  |-  ( E. y  x  =  x  ->  x  =  x )
64, 5ax-mp 8 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   E.wex 1550
This theorem is referenced by:  nfequid  1690  equcomi  1691  stdpc6  1699  19.2OLD  1713  ax9dgen  1731  ax12dgen1  1740  ax12dgen3  1742  sbid  1947  equveliOLD  2082  ax11eq  2269  exists1  2369  vjust  2949  vex  2951  reu6  3115  nfccdeq  3151  sbc8g  3160  dfnul3  3623  rab0  3640  int0  4056  dfid3  4491  isso2i  4527  reusv5OLD  4724  reusv7OLD  4726  relop  5014  f1eqcocnv  6019  fsplit  6442  mpt2xopoveq  6461  ruv  7557  dfac2  8000  konigthlem  8432  hash2prde  11676  pospo  14418  alexsubALTlem3  18068  trust  18247  isppw2  20886  nbgranself  21434  usgrasscusgra  21480  avril1  21745  mathbox  23933  foo3  23934  domep  25404  dffix2  25700  mamulid  27373  elnev  27553  ipo0  27566  ifr0  27567  tratrb  28475  tratrbVD  28827  equveliNEW7  29380
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator