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

Theorem equid 1796
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 1754 . . 3  |-  E. y 
y  =  x
2 ax-7 1795 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 47 . . 3  |-  ( y  =  x  ->  x  =  x )
41, 3eximii 1663 . 2  |-  E. y  x  =  x
5 ax5e 1711 . 2  |-  ( E. y  x  =  x  ->  x  =  x )
64, 5ax-mp 5 1  |-  x  =  x
Colors of variables: wff setvar class
Syntax hints:   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795
This theorem depends on definitions:  df-bi 185  df-ex 1618
This theorem is referenced by:  nfequid  1797  equcomi  1798  stdpc6  1805  ax6dgen  1829  ax13dgen1  1838  ax13dgen3  1840  sbid  2001  ax12eq  2273  exists1  2385  vjust  3107  vex  3109  reu6  3285  nfccdeq  3322  sbc8g  3332  dfnul3  3786  rab0  3805  int0  4285  reusv5OLD  4647  reusv7OLD  4649  dfid3  4785  isso2i  4821  relop  5142  f1eqcocnv  6179  fsplit  6878  mpt2xopoveq  6939  ruv  8018  dfac2  8502  konigthlem  8934  hash2prde  12503  pospo  15805  mamulid  19113  mdetdiagid  19272  alexsubALTlem3  20718  trust  20901  isppw2  23590  xmstrkgc  24394  nbgranself  24639  usgrasscusgra  24688  rusgrasn  25150  avril1  25376  mathbox  27562  foo3  27563  domep  29468  wlimeq12  29618  elnev  31589  ipo0  31602  ifr0  31603  tratrb  33716  tratrbVD  34081  bj-vjust  34792
  Copyright terms: Public domain W3C validator