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

Theorem equid 1681
 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 1676 . 2 𝑦 𝑦 = 𝑥
2 ax-17 1506 . . 3 (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3 ax-8 1484 . . . 4 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
43pm2.43i 49 . . 3 (𝑦 = 𝑥𝑥 = 𝑥)
52, 4exlimih 1573 . 2 (∃𝑦 𝑦 = 𝑥𝑥 = 𝑥)
61, 5ax-mp 5 1 𝑥 = 𝑥
 Colors of variables: wff set class Syntax hints:  ∃wex 1472 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  nfequid  1682  stdpc6  1683  equcomi  1684  equveli  1739  sbid  1754  ax16i  1838  exists1  2102  vjust  2713  vex  2715  reu6  2901  nfccdeq  2935  sbc8g  2944  dfnul3  3397  rab0  3422  int0  3821  ruv  4508  dcextest  4539  relop  4735  f1eqcocnv  5738  mpoxopoveq  6184  snexxph  6891
 Copyright terms: Public domain W3C validator