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

Theorem equid 1728
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 1709 . . 3  |-  E. y 
y  =  x
2 ax-7 1727 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 47 . . 3  |-  ( y  =  x  ->  x  =  x )
41, 3eximii 1628 . 2  |-  E. y  x  =  x
5 ax5e 1671 . 2  |-  ( E. y  x  =  x  ->  x  =  x )
64, 5ax-mp 5 1  |-  x  =  x
Colors of variables: wff setvar class
Syntax hints:   E.wex 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727
This theorem depends on definitions:  df-bi 185  df-ex 1590
This theorem is referenced by:  nfequid  1729  equcomi  1730  stdpc6  1737  ax6dgen  1761  ax13dgen1  1770  ax13dgen3  1772  sbid  1939  ax12eq  2243  exists1  2367  vjust  2963  vex  2965  reu6  3137  nfccdeq  3173  sbc8g  3182  dfnul3  3628  rab0  3646  int0  4130  reusv5OLD  4490  reusv7OLD  4492  dfid3  4624  isso2i  4660  relop  4977  f1eqcocnv  5986  fsplit  6666  mpt2xopoveq  6725  ruv  7804  dfac2  8288  konigthlem  8720  hash2prde  12163  pospo  15126  mamulid  18146  alexsubALTlem3  19463  trust  19646  isppw2  22338  xmstrkgc  22955  nbgranself  23168  usgrasscusgra  23214  avril1  23479  mathbox  25669  foo3  25670  domep  27453  elnev  29537  ipo0  29550  ifr0  29551  rusgrasn  30403  mdetdiagid  30667  tratrb  30964  tratrbVD  31320  bj-vjust  31949
  Copyright terms: Public domain W3C validator