![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > noel | GIF version |
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
Ref | Expression |
---|---|
noel | ⊢ ¬ A ∈ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifi 3060 | . . 3 ⊢ (A ∈ (V ∖ V) → A ∈ V) | |
2 | eldifn 3061 | . . 3 ⊢ (A ∈ (V ∖ V) → ¬ A ∈ V) | |
3 | 1, 2 | pm2.65i 567 | . 2 ⊢ ¬ A ∈ (V ∖ V) |
4 | df-nul 3219 | . . 3 ⊢ ∅ = (V ∖ V) | |
5 | 4 | eleq2i 2101 | . 2 ⊢ (A ∈ ∅ ↔ A ∈ (V ∖ V)) |
6 | 3, 5 | mtbir 595 | 1 ⊢ ¬ A ∈ ∅ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∈ wcel 1390 Vcvv 2551 ∖ cdif 2908 ∅c0 3218 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-v 2553 df-dif 2914 df-nul 3219 |
This theorem is referenced by: n0i 3223 n0rf 3227 rex0 3232 eq0 3233 abvor0dc 3236 rab0 3240 un0 3245 in0 3246 0ss 3249 disj 3262 ral0 3316 int0 3620 iun0 3704 0iun 3705 nlim0 4097 nsuceq0g 4121 ordtriexmidlem 4208 ordtriexmidlem2 4209 ordtriexmid 4210 onsucelsucexmidlem 4214 nn0eln0 4284 0xp 4363 dm0 4492 dm0rn0 4495 reldm0 4496 cnv0 4670 co02 4777 0fv 5151 acexmidlema 5446 acexmidlemb 5447 acexmidlemab 5449 mpt20 5516 nnsucelsuc 6009 nnmordi 6025 nnaordex 6036 0er 6076 elni2 6298 nlt1pig 6325 0npr 6466 fzm1 8732 frec2uzltd 8870 bdcnul 9320 bj-nnelirr 9413 |
Copyright terms: Public domain | W3C validator |