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 3239 | . . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V) | |
2 | eldifn 3240 | . . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V) | |
3 | 1, 2 | pm2.65i 629 | . 2 ⊢ ¬ 𝐴 ∈ (V ∖ V) |
4 | df-nul 3405 | . . 3 ⊢ ∅ = (V ∖ V) | |
5 | 4 | eleq2i 2231 | . 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V)) |
6 | 3, 5 | mtbir 661 | 1 ⊢ ¬ 𝐴 ∈ ∅ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∈ wcel 2135 Vcvv 2721 ∖ cdif 3108 ∅c0 3404 |
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 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-dif 3113 df-nul 3405 |
This theorem is referenced by: n0i 3409 n0rf 3416 rex0 3421 eq0 3422 abvor0dc 3427 rab0 3432 un0 3437 in0 3438 0ss 3442 disj 3452 ral0 3505 int0 3832 iun0 3916 0iun 3917 br0 4024 exmid01 4171 nlim0 4366 nsuceq0g 4390 ordtriexmidlem 4490 ordtriexmidlem2 4491 ordtriexmid 4492 ontriexmidim 4493 ordtri2or2exmidlem 4497 onsucelsucexmidlem 4500 reg2exmidlema 4505 reg3exmidlemwe 4550 nn0eln0 4591 0xp 4678 dm0 4812 dm0rn0 4815 reldm0 4816 cnv0 5001 co02 5111 0fv 5515 acexmidlema 5827 acexmidlemb 5828 acexmidlemab 5830 mpo0 5903 nnsucelsuc 6450 nnsucuniel 6454 nnmordi 6475 nnaordex 6486 0er 6526 fidcenumlemrk 6910 nnnninfeq 7083 elni2 7246 nlt1pig 7273 0npr 7415 fzm1 10025 frec2uzltd 10328 0tonninf 10364 sum0 11315 fsumsplit 11334 sumsplitdc 11359 fsum2dlemstep 11361 prod0 11512 fprod2dlemstep 11549 ennnfonelem1 12283 0ntop 12552 0met 12931 if0ab 13528 bdcnul 13588 bj-nnelirr 13676 |
Copyright terms: Public domain | W3C validator |