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

Theorem equid 1701
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 1696 . 2 𝑦 𝑦 = 𝑥
2 ax-17 1526 . . 3 (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3 ax-8 1504 . . . 4 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
43pm2.43i 49 . . 3 (𝑦 = 𝑥𝑥 = 𝑥)
52, 4exlimih 1593 . 2 (∃𝑦 𝑦 = 𝑥𝑥 = 𝑥)
61, 5ax-mp 5 1 𝑥 = 𝑥
Colors of variables: wff set class
Syntax hints:  wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  nfequid  1702  stdpc6  1703  equcomi  1704  equveli  1759  sbid  1774  ax16i  1858  exists1  2122  vjust  2738  vex  2740  reu6  2926  nfccdeq  2960  sbc8g  2970  dfnul3  3425  rab0  3451  int0  3858  ruv  4549  dcextest  4580  relop  4777  f1eqcocnv  5791  mpoxopoveq  6240  snexxph  6948
  Copyright terms: Public domain W3C validator