![]() |
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 3726 |
. . 3
![]() ![]() ![]() ![]() ![]() | |
2 | eleq2 2538 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mtbiri 310 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2i 124 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-v 3033 df-dif 3393 df-nul 3723 |
This theorem is referenced by: ne0i 3728 oprcl 4183 disjss3 4394 iin0 4575 snsn0non 5548 mptrcl 5970 isomin 6246 ovrcl 6341 tfrlem16 7129 oalimcl 7279 omlimcl 7297 oaabs2 7364 ecexr 7386 elpmi 7508 elmapex 7510 pmresg 7517 pmsspw 7524 ixpssmap2g 7569 ixpssmapg 7570 resixpfo 7578 php3 7776 cantnfp1lem2 8202 cantnflem1 8212 cnfcom2lem 8224 rankxplim2 8369 rankxplim3 8370 cardlim 8424 alephnbtwn 8520 pwcdadom 8664 ttukeylem5 8961 r1wunlim 9180 nnunb 10889 ssnn0fi 12235 ruclem13 14371 ramtub 15047 ramtubOLD 15048 elbasfv 15248 elbasov 15249 restsspw 15408 homarcl 16001 grpidval 16581 odlem2 17266 odlem2OLD 17282 efgrelexlema 17477 subcmn 17555 dvdsrval 17951 pf1rcl 19014 elocv 19308 matrcl 19514 0top 20076 ppttop 20099 pptbas 20100 restrcl 20250 ssrest 20269 iscnp2 20332 lmmo 20473 zfbas 20989 rnelfmlem 21045 isfcls 21102 isnghm 21806 isnghmOLD 21824 iscau2 22325 itg2cnlem1 22798 itgsubstlem 23079 dchrrcl 24247 eleenn 25005 nbgranself2 25243 uvtxisvtx 25297 uvtx01vtx 25299 2spot0 25871 hon0 27527 dmadjrnb 27640 eulerpartlemgvv 29282 bnj98 29750 indispcon 30029 cvmtop1 30055 cvmtop2 30056 mrsub0 30226 mrsubf 30227 mrsubccat 30228 mrsubcn 30229 mrsubco 30231 mrsubvrs 30232 msubf 30242 mclsrcl 30271 funpartlem 30780 tailfb 31104 atbase 32926 llnbase 33145 lplnbase 33170 lvolbase 33214 osumcllem4N 33595 pexmidlem1N 33606 lhpbase 33634 mapco2g 35627 wepwsolem 35971 ssfiunibd 37615 hoicvr 38488 |
Copyright terms: Public domain | W3C validator |