![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > noel | Structured version Visualization version Unicode 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 3555 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eldifn 3556 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | pm2.65i 177 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-nul 3732 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | eleq2i 2521 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | mtbir 301 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-v 3047 df-dif 3407 df-nul 3732 |
This theorem is referenced by: n0i 3736 n0f 3740 rex0 3746 abvor0 3750 rab0 3753 un0 3759 in0 3760 0ss 3763 sbcel12 3772 sbcel2 3778 disj 3805 r19.2zb 3859 ral0 3874 rabsnifsb 4040 int0 4248 iun0 4334 0iun 4335 br0 4449 pwne0 4573 0xp 4915 csbxp 4916 dm0 5048 dm0rn0 5051 reldm0 5052 elimasni 5195 cnv0 5239 co02 5349 ord0eln0 5477 nlim0 5481 nsuceq0 5503 dffv3 5861 0fv 5898 mpt20 6361 bropopvvv 6874 bropfvvvv 6876 tz7.44-2 7125 omordi 7267 omeulem1 7283 nnmordi 7332 omabs 7348 omsmolem 7354 0er 7398 omxpenlem 7673 en3lp 8121 cantnfle 8176 r1sdom 8245 r1pwss 8255 alephordi 8505 axdc3lem2 8881 zorn2lem7 8932 nlt1pi 9331 xrinf0 11623 xrinfm0OLD 11627 elixx3g 11648 elfz2 11791 fzm1 11874 om2uzlti 12164 hashf1lem2 12619 sum0 13787 fsumsplit 13806 sumsplit 13829 fsum2dlem 13831 prod0 13997 fprod2dlem 14034 sadc0 14428 sadcp1 14429 saddisjlem 14438 smu01lem 14459 smu01 14460 smu02 14461 lcmf0 14607 prmreclem5 14864 vdwap0 14926 ram0 14980 0catg 15593 oduclatb 16390 0g0 16506 cntzrcl 16981 pmtrfrn 17099 psgnunilem5 17135 gexdvds 17235 gsumzsplit 17560 dprdcntz2 17671 00lss 18165 mplcoe1 18689 mplcoe5 18692 00ply1bas 18833 dsmmbas2 19300 dsmmfi 19301 maducoeval2 19665 madugsum 19668 0ntop 19935 haust1 20368 hauspwdom 20516 kqcldsat 20748 tsmssplit 21166 ustn0 21235 0met 21381 itg11 22649 itg0 22737 bddmulibl 22796 fsumharmonic 23937 ppiublem2 24131 lgsdir2lem3 24253 nbgra0edg 25160 uvtx01vtx 25220 clwwlknprop 25500 2wlkonot3v 25603 2spthonot3v 25604 rusgra0edg 25683 eupath2lem1 25705 helloworld 25902 topnfbey 25906 isarchi 28499 measvuni 29036 ddemeas 29059 sibf0 29167 signstfvneq0 29461 opelco3 30420 wsuclem 30508 bj-projval 31590 bj-df-nul 31621 bj-nuliota 31623 finxp0 31783 poimirlem30 31970 pw2f1ocnv 35892 areaquad 36101 en3lpVD 37241 iblempty 37842 stoweidlem34 37895 sge00 38218 uvtxa01vtx0 39469 vtxdg0v 39533 |
Copyright terms: Public domain | W3C validator |