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

Theorem equid 1683
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 WolfLammen, 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 1663 . . 3  |-  E. y 
y  =  x
2 ax-8 1682 . . . 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  1685  equcomi  1686  stdpc6  1694  19.2OLD  1707  ax9dgen  1723  ax12dgen1  1732  ax12dgen3  1734  sbid  1936  equveli  2023  ax11eq  2227  exists1  2327  vjust  2900  vex  2902  reu6  3066  nfccdeq  3102  sbc8g  3111  dfnul3  3574  rab0  3591  int0  4006  dfid3  4440  isso2i  4476  reusv5OLD  4673  reusv7OLD  4675  relop  4963  f1eqcocnv  5967  fsplit  6390  mpt2xopoveq  6406  ruv  7501  dfac2  7944  konigthlem  8376  hash2prde  11615  pospo  14357  alexsubALTlem3  18001  trust  18180  isppw2  20765  nbgranself  21312  usgrasscusgra  21358  avril1  21605  mathbox  23793  foo3  23794  domep  25173  dffix2  25469  mamulid  27127  elnev  27307  ipo0  27320  ifr0  27321  tratrb  27963  tratrbVD  28314  equveliNEW7  28864
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 1661  ax-8 1682
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator