Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > n0i | Structured version Visualization version Unicode version |
Description: If a set has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
n0i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 3919 | . . 3 | |
2 | eleq2 2690 | . . 3 | |
3 | 1, 2 | mtbiri 317 | . 2 |
4 | 3 | con2i 134 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wceq 1483 wcel 1990 c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-nul 3916 |
This theorem is referenced by: ne0i 3921 n0ii 3922 oprcl 4427 disjss3 4652 mptrcl 6289 isomin 6587 ovrcl 6686 oalimcl 7640 omlimcl 7658 oaabs2 7725 ecexr 7747 elpmi 7876 elmapex 7878 pmresg 7885 pmsspw 7892 ixpssmap2g 7937 ixpssmapg 7938 resixpfo 7946 php3 8146 cantnfp1lem2 8576 cantnflem1 8586 cnfcom2lem 8598 rankxplim2 8743 rankxplim3 8744 cardlim 8798 alephnbtwn 8894 ttukeylem5 9335 r1wunlim 9559 ssnn0fi 12784 ruclem13 14971 ramtub 15716 elbasfv 15920 elbasov 15921 restsspw 16092 homarcl 16678 grpidval 17260 odlem2 17958 efgrelexlema 18162 subcmn 18242 dvdsrval 18645 pf1rcl 19713 elocv 20012 matrcl 20218 0top 20787 ppttop 20811 pptbas 20812 restrcl 20961 ssrest 20980 iscnp2 21043 lmmo 21184 zfbas 21700 rnelfmlem 21756 isfcls 21813 isnghm 22527 iscau2 23075 itg2cnlem1 23528 itgsubstlem 23811 dchrrcl 24965 eleenn 25776 eulerpartlemgvv 30438 indispconn 31216 cvmtop1 31242 cvmtop2 31243 mrsub0 31413 mrsubf 31414 mrsubccat 31415 mrsubcn 31416 mrsubco 31418 mrsubvrs 31419 msubf 31429 mclsrcl 31458 funpartlem 32049 tailfb 32372 atbase 34576 llnbase 34795 lplnbase 34820 lvolbase 34864 osumcllem4N 35245 pexmidlem1N 35256 lhpbase 35284 mapco2g 37277 wepwsolem 37612 uneqsn 38321 ssfiunibd 39523 hoicvr 40762 |
Copyright terms: Public domain | W3C validator |