![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > ne0ii | Unicode version |
Description: If a set has elements, then it is not empty. Inference associated with ne0i 3790. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
ne0ii.1 |
Ref | Expression |
---|---|
ne0ii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ne0ii.1 | . 2 | |
2 | ne0i 3790 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: e. wcel 1818 =/= wne 2652
c0 3784 |
This theorem is referenced by: vn0 3792 prnz 4149 tpnz 4151 onn0 4947 oawordeulem 7222 noinfep 8097 fin23lem31 8744 isfin1-3 8787 omina 9090 rpnnen1lem4 11240 rpnnen1lem5 11241 rexfiuz 13180 caurcvg 13499 caurcvg2 13500 caucvg 13501 infcvgaux1i 13668 divalglem2 14053 pc2dvds 14402 vdwmc2 14497 cnsubglem 18467 cnmsubglem 18480 pmatcollpw3 19285 zfbas 20397 nrginvrcn 21200 lebnumlem3 21463 caun0 21720 cnflduss 21796 cnfldcusp 21797 reust 21813 recusp 21814 nulmbl2 21947 itg2seq 22149 itg2monolem1 22157 c1lip1 22398 aannenlem2 22725 shintcl 26248 chintcl 26250 nmoprepnf 26786 nmfnrepnf 26799 nmcexi 26945 snct 27534 esum0 28060 esumpcvgval 28084 ismblfin 30055 volsupnfl 30059 itg2addnclem 30066 ftc1anc 30098 incsequz 30241 isbnd3 30280 ssbnd 30284 ioodvbdlimc1 31730 ioodvbdlimc2 31732 dvnprodlem3 31745 stirlinglem13 31868 fourierdlem103 31992 fourierdlem104 31993 fouriersw 32014 2zlidl 32740 bnj906 33988 bj-tagn0 34537 taupi 37698 imo72b2lem0 37982 imo72b2lem2 37984 imo72b2lem1 37988 imo72b2 37993 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-v 3111 df-dif 3478 df-nul 3785 |
Copyright terms: Public domain | W3C validator |