![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > noel | Structured version Visualization version GIF version |
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
Ref | Expression |
---|---|
noel | ⊢ ¬ 𝐴 ∈ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifi 3863 | . . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V) | |
2 | eldifn 3864 | . . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V) | |
3 | 1, 2 | pm2.65i 185 | . 2 ⊢ ¬ 𝐴 ∈ (V ∖ V) |
4 | df-nul 4047 | . . 3 ⊢ ∅ = (V ∖ V) | |
5 | 4 | eleq2i 2819 | . 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V)) |
6 | 3, 5 | mtbir 312 | 1 ⊢ ¬ 𝐴 ∈ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2127 Vcvv 3328 ∖ cdif 3700 ∅c0 4046 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-v 3330 df-dif 3706 df-nul 4047 |
This theorem is referenced by: n0i 4051 eq0f 4056 n0fOLD 4059 rex0 4069 rab0 4086 rab0OLD 4087 un0 4098 in0 4099 0ss 4103 sbcel12 4114 sbcel2 4120 disj 4148 r19.2zb 4193 ral0 4208 rabsnifsb 4389 int0OLD 4631 iun0 4716 br0 4841 0xp 5344 csbxp 5345 dm0 5482 dm0rn0 5485 reldm0 5486 elimasni 5638 cnv0OLD 5682 co02 5798 ord0eln0 5928 nlim0 5932 nsuceq0 5954 dffv3 6336 0fv 6376 elfv2ex 6378 mpt20 6878 el2mpt2csbcl 7406 bropopvvv 7411 bropfvvvv 7413 tz7.44-2 7660 omordi 7803 omeulem1 7819 nnmordi 7868 omabs 7884 omsmolem 7890 0er 7936 omxpenlem 8214 en3lp 8670 cantnfle 8729 r1sdom 8798 r1pwss 8808 alephordi 9058 axdc3lem2 9436 zorn2lem7 9487 nlt1pi 9891 xrinf0 12332 elixx3g 12352 elfz2 12497 fzm1 12584 om2uzlti 12914 hashf1lem2 13403 sum0 14622 fsumsplit 14641 sumsplit 14669 fsum2dlem 14671 prod0 14843 fprod2dlem 14880 sadc0 15349 sadcp1 15350 saddisjlem 15359 smu01lem 15380 smu01 15381 smu02 15382 lcmf0 15520 prmreclem5 15797 vdwap0 15853 ram0 15899 0catg 16520 oduclatb 17316 0g0 17435 dfgrp2e 17620 cntzrcl 17931 pmtrfrn 18049 psgnunilem5 18085 gexdvds 18170 gsumzsplit 18498 dprdcntz2 18608 00lss 19115 mplcoe1 19638 mplcoe5 19641 00ply1bas 19783 dsmmbas2 20254 dsmmfi 20255 maducoeval2 20619 madugsum 20622 0ntop 20883 haust1 21329 hauspwdom 21477 kqcldsat 21709 tsmssplit 22127 ustn0 22196 0met 22343 itg11 23628 itg0 23716 bddmulibl 23775 fsumharmonic 24908 ppiublem2 25098 lgsdir2lem3 25222 uvtx01vtx 26471 uvtxa01vtx0OLD 26473 vtxdg0v 26550 0enwwlksnge1 26944 rusgr0edg 27066 clwwlk 27077 eupth2lem1 27341 helloworld 27603 topnfbey 27607 n0lpligALT 27618 isarchi 30016 measvuni 30557 ddemeas 30579 sibf0 30676 signstfvneq0 30929 opelco3 31954 wsuclem 32047 unbdqndv1 32776 bj-projval 33261 bj-df-nul 33294 bj-nuliota 33296 bj-0nmoore 33344 poimirlem30 33721 nel02 34390 pw2f1ocnv 38075 areaquad 38273 ntrneikb 38863 en3lpVD 39548 supminfxr 40161 liminf0 40497 iblempty 40653 stoweidlem34 40723 sge00 41065 vonhoire 41361 |
Copyright terms: Public domain | W3C validator |