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

Theorem equid 1729
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 1710 . . 3  |-  E. y 
y  =  x
2 ax-7 1728 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 47 . . 3  |-  ( y  =  x  ->  x  =  x )
41, 3eximii 1627 . 2  |-  E. y  x  =  x
5 ax5e 1672 . 2  |-  ( E. y  x  =  x  ->  x  =  x )
64, 5ax-mp 5 1  |-  x  =  x
Colors of variables: wff setvar class
Syntax hints:   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  nfequid  1730  equcomi  1731  stdpc6  1738  ax6dgen  1762  ax13dgen1  1771  ax13dgen3  1773  sbid  1940  ax12eq  2242  exists1  2376  vjust  2976  vex  2978  reu6  3151  nfccdeq  3187  sbc8g  3197  dfnul3  3643  rab0  3661  int0  4145  reusv5OLD  4505  reusv7OLD  4507  dfid3  4640  isso2i  4676  relop  4993  f1eqcocnv  6002  fsplit  6680  mpt2xopoveq  6739  ruv  7819  dfac2  8303  konigthlem  8735  hash2prde  12182  pospo  15146  mamulid  18307  alexsubALTlem3  19624  trust  19807  isppw2  22456  xmstrkgc  23135  nbgranself  23348  usgrasscusgra  23394  avril1  23659  mathbox  25849  foo3  25850  domep  27609  elnev  29695  ipo0  29708  ifr0  29709  rusgrasn  30560  mdetdiagid  30940  tratrb  31245  tratrbVD  31600  bj-vjust  32310
  Copyright terms: Public domain W3C validator