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

Theorem equid 1605
 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 1602 . 2 𝑦 𝑦 = 𝑥
2 ax-17 1435 . . 3 (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥)
3 ax-8 1411 . . . 4 (𝑦 = 𝑥 → (𝑦 = 𝑥𝑥 = 𝑥))
43pm2.43i 47 . . 3 (𝑦 = 𝑥𝑥 = 𝑥)
52, 4exlimih 1500 . 2 (∃𝑦 𝑦 = 𝑥𝑥 = 𝑥)
61, 5ax-mp 7 1 𝑥 = 𝑥
 Colors of variables: wff set class Syntax hints:  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-gen 1354  ax-ie2 1399  ax-8 1411  ax-17 1435  ax-i9 1439 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  nfequid  1606  stdpc6  1607  equcomi  1608  equveli  1658  sbid  1673  ax16i  1754  exists1  2012  vjust  2575  vex  2577  reu6  2753  nfccdeq  2785  sbc8g  2794  dfnul3  3255  rab0  3274  int0  3657  ruv  4302  relop  4514  f1eqcocnv  5459  mpt2xopoveq  5886
 Copyright terms: Public domain W3C validator