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

Theorem equid 1571
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 . 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

Proof of Theorem equid
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 a9e 1568 . 2
2 ax-17 1400 . . 3
3 ax-8 1376 . . . 4
43pm2.43i 43 . . 3
52, 4exlimih 1466 . 2
61, 5ax-mp 7 1
Colors of variables: wff set class
Syntax hints:  wex 1362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1318  ax-ie2 1364  ax-8 1376  ax-17 1400  ax-i9 1404
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nfequid  1572  stdpc6  1573  equcomi  1574  equveli  1624  sbid  1639  ax16i  1720  exists1  1978  vjust  2536  vex  2538  reu6  2707  nfccdeq  2739  sbc8g  2748  dfnul3  3204  rab0  3223  int0  3603  ruv  4212  relop  4413  f1eqcocnv  5356  mpt2xopoveq  5777  mathbox  7149
  Copyright terms: Public domain W3C validator