![]() |
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 3734 |
. . 3
![]() ![]() ![]() ![]() ![]() | |
2 | eleq2 2517 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mtbiri 305 |
. 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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-v 3046 df-dif 3406 df-nul 3731 |
This theorem is referenced by: ne0i 3736 oprcl 4190 disjss3 4400 iin0 4576 snsn0non 5540 mptrcl 5953 isomin 6226 ovrcl 6321 tfrlem16 7108 oalimcl 7258 omlimcl 7276 oaabs2 7343 ecexr 7365 elpmi 7487 elmapex 7489 pmresg 7496 pmsspw 7503 ixpssmap2g 7548 ixpssmapg 7549 resixpfo 7557 php3 7755 cantnfp1lem2 8181 cantnflem1 8191 cnfcom2lem 8203 rankxplim2 8348 rankxplim3 8349 cardlim 8403 alephnbtwn 8499 pwcdadom 8643 ttukeylem5 8940 r1wunlim 9159 nnunb 10862 ssnn0fi 12194 ruclem13 14287 ramtub 14961 ramtubOLD 14962 elbasfv 15163 elbasov 15164 restsspw 15323 homarcl 15916 grpidval 16496 odlem2 17181 odlem2OLD 17197 efgrelexlema 17392 subcmn 17470 dvdsrval 17866 pf1rcl 18930 elocv 19224 matrcl 19430 0top 19992 ppttop 20015 pptbas 20016 restrcl 20166 ssrest 20185 iscnp2 20248 lmmo 20389 zfbas 20904 rnelfmlem 20960 isfcls 21017 isnghm 21721 isnghmOLD 21739 iscau2 22240 itg2cnlem1 22712 itgsubstlem 22993 dchrrcl 24161 eleenn 24919 nbgranself2 25157 uvtxisvtx 25211 uvtx01vtx 25213 2spot0 25785 hon0 27439 dmadjrnb 27552 eulerpartlemgvv 29202 bnj98 29671 indispcon 29950 cvmtop1 29976 cvmtop2 29977 mrsub0 30147 mrsubf 30148 mrsubccat 30149 mrsubcn 30150 mrsubco 30152 mrsubvrs 30153 msubf 30163 mclsrcl 30192 funpartlem 30702 tailfb 31026 atbase 32849 llnbase 33068 lplnbase 33093 lvolbase 33137 osumcllem4N 33518 pexmidlem1N 33529 lhpbase 33557 mapco2g 35550 wepwsolem 35894 ssfiunibd 37521 hoicvr 38364 |
Copyright terms: Public domain | W3C validator |