Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > equid | Unicode 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 1674 | . 2 | |
2 | ax-17 1506 | . . 3 | |
3 | ax-8 1482 | . . . 4 | |
4 | 3 | pm2.43i 49 | . . 3 |
5 | 2, 4 | exlimih 1572 | . 2 |
6 | 1, 5 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-gen 1425 ax-ie2 1470 ax-8 1482 ax-17 1506 ax-i9 1510 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nfequid 1678 stdpc6 1679 equcomi 1680 equveli 1732 sbid 1747 ax16i 1830 exists1 2093 vjust 2682 vex 2684 reu6 2868 nfccdeq 2902 sbc8g 2911 dfnul3 3361 rab0 3386 int0 3780 ruv 4460 dcextest 4490 relop 4684 f1eqcocnv 5685 mpoxopoveq 6130 snexxph 6831 |
Copyright terms: Public domain | W3C validator |