ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  equid Unicode version

Theorem equid 1634
Description: Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms.

This proof is similar to Tarski's and makes use of a dummy variable  y. It also works in intuitionistic logic, unlike some other possible ways of proving this theorem. (Contributed by NM, 1-Apr-2005.)

Assertion
Ref Expression
equid  |-  x  =  x

Proof of Theorem equid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 a9e 1631 . 2  |-  E. y 
y  =  x
2 ax-17 1464 . . 3  |-  ( x  =  x  ->  A. y  x  =  x )
3 ax-8 1440 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
43pm2.43i 48 . . 3  |-  ( y  =  x  ->  x  =  x )
52, 4exlimih 1529 . 2  |-  ( E. y  y  =  x  ->  x  =  x )
61, 5ax-mp 7 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   E.wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1383  ax-ie2 1428  ax-8 1440  ax-17 1464  ax-i9 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nfequid  1635  stdpc6  1636  equcomi  1637  equveli  1689  sbid  1704  ax16i  1786  exists1  2044  vjust  2620  vex  2622  reu6  2802  nfccdeq  2836  sbc8g  2845  dfnul3  3287  rab0  3309  int0  3697  ruv  4356  dcextest  4386  relop  4574  f1eqcocnv  5552  mpt2xopoveq  5987  snexxph  6638
  Copyright terms: Public domain W3C validator