![]() |
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 2739 vex 2741 reu6 2927 nfccdeq 2961 sbc8g 2971 dfnul3 3426 rab0 3452 int0 3859 ruv 4550 dcextest 4581 relop 4778 f1eqcocnv 5792 mpoxopoveq 6241 snexxph 6949 |
Copyright terms: Public domain | W3C validator |