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

Theorem equid 1529
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 1527 . 2 y y = x
2 ax-17 1367 . . 3 (x = xy x = x)
3 ax-8 1344 . . . 4 (y = x → (y = xx = x))
43pm2.43i 41 . . 3 (y = xx = x)
52, 4exlimih 1430 . 2 (y y = xx = x)
61, 5ax-mp 7 1 x = x
Colors of variables: wff set class
Syntax hints:  wex 1328
This theorem is referenced by:  nfequid  1530  stdpc6  1531  equcomi  1532  equveli  1582  sbid  1597  ax16i  1677  exists1  1926  vjust  2442  vex  2444  reu6  2610  nfccdeq  2642  sbc8g  2651  dfnul3  3112  rab0  3129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-gen 1284  ax-ie2 1330  ax-8 1344  ax-17 1367  ax-i9 1371
This theorem depends on definitions:  df-bi 108
  Copyright terms: Public domain W3C validator