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

Theorem equid 1630
 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 1627 . 2 𝑦 𝑦 = 𝑥
2 ax-17 1460 . . 3 (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3 ax-8 1436 . . . 4 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
43pm2.43i 48 . . 3 (𝑦 = 𝑥𝑥 = 𝑥)
52, 4exlimih 1525 . 2 (∃𝑦 𝑦 = 𝑥𝑥 = 𝑥)
61, 5ax-mp 7 1 𝑥 = 𝑥
 Colors of variables: wff set class Syntax hints:  ∃wex 1422 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  nfequid  1631  stdpc6  1632  equcomi  1633  equveli  1684  sbid  1699  ax16i  1781  exists1  2039  vjust  2613  vex  2615  reu6  2792  nfccdeq  2824  sbc8g  2833  dfnul3  3272  rab0  3294  int0  3676  ruv  4329  dcextest  4359  relop  4544  f1eqcocnv  5510  mpt2xopoveq  5937  snexxph  6583
 Copyright terms: Public domain W3C validator