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

Theorem equid 1605
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 1602 . 2  |-  E. y 
y  =  x
2 ax-17 1435 . . 3  |-  ( x  =  x  ->  A. y  x  =  x )
3 ax-8 1411 . . . 4  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
43pm2.43i 47 . . 3  |-  ( y  =  x  ->  x  =  x )
52, 4exlimih 1500 . 2  |-  ( E. y  y  =  x  ->  x  =  x )
61, 5ax-mp 7 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   E.wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-gen 1354  ax-ie2 1399  ax-8 1411  ax-17 1435  ax-i9 1439
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  nfequid  1606  stdpc6  1607  equcomi  1608  equveli  1658  sbid  1673  ax16i  1754  exists1  2012  vjust  2575  vex  2577  reu6  2752  nfccdeq  2784  sbc8g  2793  dfnul3  3254  rab0  3273  int0  3656  ruv  4301  relop  4513  f1eqcocnv  5458  mpt2xopoveq  5885
  Copyright terms: Public domain W3C validator