![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equid | GIF version |
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.) |
Ref | Expression |
---|---|
equid | ⊢ 𝑥 = 𝑥 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a9e 1696 | . 2 ⊢ ∃𝑦 𝑦 = 𝑥 | |
2 | ax-17 1526 | . . 3 ⊢ (𝑥 = 𝑥 → ∀𝑦 𝑥 = 𝑥) | |
3 | ax-8 1504 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥)) | |
4 | 3 | pm2.43i 49 | . . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥) |
5 | 2, 4 | exlimih 1593 | . 2 ⊢ (∃𝑦 𝑦 = 𝑥 → 𝑥 = 𝑥) |
6 | 1, 5 | ax-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 |