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

Theorem equid 1740
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 ax6ev 1721 . . 3  |-  E. y 
y  =  x
2 ax-7 1739 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 47 . . 3  |-  ( y  =  x  ->  x  =  x )
41, 3eximii 1637 . 2  |-  E. y  x  =  x
5 ax5e 1682 . 2  |-  ( E. y  x  =  x  ->  x  =  x )
64, 5ax-mp 5 1  |-  x  =  x
Colors of variables: wff setvar class
Syntax hints:   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  nfequid  1741  equcomi  1742  stdpc6  1749  ax6dgen  1773  ax13dgen1  1782  ax13dgen3  1784  sbid  1965  ax12eq  2264  exists1  2398  vjust  3114  vex  3116  reu6  3292  nfccdeq  3329  sbc8g  3339  dfnul3  3788  rab0  3806  int0  4296  reusv5OLD  4657  reusv7OLD  4659  dfid3  4796  isso2i  4832  relop  5151  f1eqcocnv  6190  fsplit  6885  mpt2xopoveq  6944  ruv  8023  dfac2  8507  konigthlem  8939  hash2prde  12478  pospo  15456  mamulid  18710  mdetdiagid  18869  alexsubALTlem3  20284  trust  20467  isppw2  23117  xmstrkgc  23865  nbgranself  24110  usgrasscusgra  24159  rusgrasn  24621  avril1  24847  mathbox  27037  foo3  27038  domep  28802  elnev  30923  ipo0  30936  ifr0  30937  tratrb  32386  tratrbVD  32741  bj-vjust  33453
  Copyright terms: Public domain W3C validator