Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ne0ii | Structured version Visualization version Unicode version |
Description: If a set has elements, then it is not empty. Inference associated with ne0i 3921. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
n0ii.1 |
Ref | Expression |
---|---|
ne0ii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0ii.1 | . 2 | |
2 | ne0i 3921 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 wne 2794 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-ne 2795 df-v 3202 df-dif 3577 df-nul 3916 |
This theorem is referenced by: vn0 3924 prnz 4310 tpnz 4313 pwne0 4835 onn0 5789 oawordeulem 7634 noinfep 8557 fin23lem31 9165 isfin1-3 9208 omina 9513 rpnnen1lem4 11817 rpnnen1lem5 11818 rpnnen1lem4OLD 11823 rpnnen1lem5OLD 11824 rexfiuz 14087 caurcvg 14407 caurcvg2 14408 caucvg 14409 infcvgaux1i 14589 divalglem2 15118 pc2dvds 15583 vdwmc2 15683 cnsubglem 19795 cnmsubglem 19809 pmatcollpw3 20589 zfbas 21700 nrginvrcn 22496 lebnumlem3 22762 caun0 23079 cnflduss 23152 cnfldcusp 23153 reust 23169 recusp 23170 nulmbl2 23304 itg2seq 23509 itg2monolem1 23517 c1lip1 23760 aannenlem2 24084 logbmpt 24526 tgcgr4 25426 shintcl 28189 chintcl 28191 nmoprepnf 28726 nmfnrepnf 28739 nmcexi 28885 snct 29491 esum0 30111 esumpcvgval 30140 bnj906 31000 bj-tagn0 32967 taupi 33169 ismblfin 33450 volsupnfl 33454 itg2addnclem 33461 ftc1anc 33493 incsequz 33544 isbnd3 33583 ssbnd 33587 corclrcl 37999 imo72b2lem0 38465 imo72b2lem2 38467 imo72b2lem1 38471 imo72b2 38475 amgm2d 38501 nnn0 39595 ren0 39626 ioodvbdlimc1 40148 ioodvbdlimc2 40150 stirlinglem13 40303 fourierdlem103 40426 fourierdlem104 40427 fouriersw 40448 hoicvr 40762 2zlidl 41934 |
Copyright terms: Public domain | W3C validator |