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 | ⊢ ¬ 𝐴 ∈ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifi 3168 | . . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V) | |
2 | eldifn 3169 | . . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V) | |
3 | 1, 2 | pm2.65i 613 | . 2 ⊢ ¬ 𝐴 ∈ (V ∖ V) |
4 | df-nul 3334 | . . 3 ⊢ ∅ = (V ∖ V) | |
5 | 4 | eleq2i 2184 | . 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V)) |
6 | 3, 5 | mtbir 645 | 1 ⊢ ¬ 𝐴 ∈ ∅ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∈ wcel 1465 Vcvv 2660 ∖ cdif 3038 ∅c0 3333 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-dif 3043 df-nul 3334 |
This theorem is referenced by: n0i 3338 n0rf 3345 rex0 3350 eq0 3351 abvor0dc 3356 rab0 3361 un0 3366 in0 3367 0ss 3371 disj 3381 ral0 3434 int0 3755 iun0 3839 0iun 3840 br0 3946 exmid01 4091 nlim0 4286 nsuceq0g 4310 ordtriexmidlem 4405 ordtriexmidlem2 4406 ordtriexmid 4407 ordtri2or2exmidlem 4411 onsucelsucexmidlem 4414 reg2exmidlema 4419 reg3exmidlemwe 4463 nn0eln0 4503 0xp 4589 dm0 4723 dm0rn0 4726 reldm0 4727 cnv0 4912 co02 5022 0fv 5424 acexmidlema 5733 acexmidlemb 5734 acexmidlemab 5736 mpo0 5809 nnsucelsuc 6355 nnsucuniel 6359 nnmordi 6380 nnaordex 6391 0er 6431 fidcenumlemrk 6810 elni2 7090 nlt1pig 7117 0npr 7259 fzm1 9848 frec2uzltd 10144 0tonninf 10180 sum0 11125 fsumsplit 11144 sumsplitdc 11169 fsum2dlemstep 11171 ennnfonelem1 11847 0ntop 12101 0met 12480 bdcnul 12990 bj-nnelirr 13078 nninfalllemn 13129 |
Copyright terms: Public domain | W3C validator |