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

Theorem equid 1662
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 1659 . 2 𝑦 𝑦 = 𝑥
2 ax-17 1491 . . 3 (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3 ax-8 1467 . . . 4 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
43pm2.43i 49 . . 3 (𝑦 = 𝑥𝑥 = 𝑥)
52, 4exlimih 1557 . 2 (∃𝑦 𝑦 = 𝑥𝑥 = 𝑥)
61, 5ax-mp 5 1 𝑥 = 𝑥
Colors of variables: wff set class
Syntax hints:  wex 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1410  ax-ie2 1455  ax-8 1467  ax-17 1491  ax-i9 1495
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  nfequid  1663  stdpc6  1664  equcomi  1665  equveli  1717  sbid  1732  ax16i  1814  exists1  2073  vjust  2661  vex  2663  reu6  2846  nfccdeq  2880  sbc8g  2889  dfnul3  3336  rab0  3361  int0  3755  ruv  4435  dcextest  4465  relop  4659  f1eqcocnv  5660  mpoxopoveq  6105  snexxph  6806
  Copyright terms: Public domain W3C validator