New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > equid1 | 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 (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and thus requires no dummy variables. A simpler proof, similar to Tarki's, is possible if we make use of ax-17 1616; see the proof of equid 1676. See equid1ALT 2176 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
equid1 | ⊢ x = x |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5o 2136 | . . . 4 ⊢ (∀x(∀x ¬ ∀x x = x → (x = x → ∀x x = x)) → (∀x ¬ ∀x x = x → ∀x(x = x → ∀x x = x))) | |
2 | ax-4 2135 | . . . . 5 ⊢ (∀x ¬ ∀x x = x → ¬ ∀x x = x) | |
3 | ax-12o 2142 | . . . . 5 ⊢ (¬ ∀x x = x → (¬ ∀x x = x → (x = x → ∀x x = x))) | |
4 | 2, 2, 3 | sylc 56 | . . . 4 ⊢ (∀x ¬ ∀x x = x → (x = x → ∀x x = x)) |
5 | 1, 4 | mpg 1548 | . . 3 ⊢ (∀x ¬ ∀x x = x → ∀x(x = x → ∀x x = x)) |
6 | ax-9o 2138 | . . 3 ⊢ (∀x(x = x → ∀x x = x) → x = x) | |
7 | 5, 6 | syl 15 | . 2 ⊢ (∀x ¬ ∀x x = x → x = x) |
8 | ax-6o 2137 | . 2 ⊢ (¬ ∀x ¬ ∀x x = x → x = x) | |
9 | 7, 8 | pm2.61i 156 | 1 ⊢ x = x |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-4 2135 ax-5o 2136 ax-6o 2137 ax-9o 2138 ax-12o 2142 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |