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

Theorem equid 1572
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 1569 . 2 y y = x
2 ax-17 1401 . . 3 (x = xy x = x)
3 ax-8 1377 . . . 4 (y = x → (y = xx = x))
43pm2.43i 43 . . 3 (y = xx = x)
52, 4exlimih 1468 . 2 (y y = xx = x)
61, 5ax-mp 7 1 x = x
Colors of variables: wff set class
Syntax hints:  wex 1363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1318  ax-ie2 1365  ax-8 1377  ax-17 1401  ax-i9 1405
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nfequid  1573  stdpc6  1574  equcomi  1575  equveli  1625  sbid  1640  ax16i  1721  exists1  1979  vjust  2535  vex  2537  reu6  2706  nfccdeq  2738  sbc8g  2747  dfnul3  3203  rab0  3222  int0  3602  ruv  4210  relop  4411  f1eqcocnv  5354  mpt2xopoveq  5774  mathbox  6355
  Copyright terms: Public domain W3C validator