MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equid Structured version   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  2086  ax11eq  2270  exists1  2370  vjust  2957  vex  2959  reu6  3123  nfccdeq  3159  sbc8g  3168  dfnul3  3631  rab0  3648  int0  4064  dfid3  4499  isso2i  4535  reusv5OLD  4733  reusv7OLD  4735  relop  5023  f1eqcocnv  6028  fsplit  6451  mpt2xopoveq  6470  ruv  7568  dfac2  8011  konigthlem  8443  hash2prde  11688  pospo  14430  alexsubALTlem3  18080  trust  18259  isppw2  20898  nbgranself  21446  usgrasscusgra  21492  avril1  21757  mathbox  23945  foo3  23946  domep  25420  mamulid  27435  elnev  27615  ipo0  27628  ifr0  27629  tratrb  28620  tratrbVD  28973  equveliNEW7  29528
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