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 1683 | . 2 | |
2 | ax-17 1513 | . . 3 | |
3 | ax-8 1491 | . . . 4 | |
4 | 3 | pm2.43i 49 | . . 3 |
5 | 2, 4 | exlimih 1580 | . 2 |
6 | 1, 5 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wex 1479 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-gen 1436 ax-ie2 1481 ax-8 1491 ax-17 1513 ax-i9 1517 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nfequid 1689 stdpc6 1690 equcomi 1691 equveli 1746 sbid 1761 ax16i 1845 exists1 2109 vjust 2722 vex 2724 reu6 2910 nfccdeq 2944 sbc8g 2953 dfnul3 3407 rab0 3432 int0 3832 ruv 4521 dcextest 4552 relop 4748 f1eqcocnv 5753 mpoxopoveq 6199 snexxph 6906 |
Copyright terms: Public domain | W3C validator |