![]() |
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 3739. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
ne0ii.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ne0ii |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ne0ii.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | ne0i 3739 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-v 3049 df-dif 3409 df-nul 3734 |
This theorem is referenced by: vn0 3741 prnz 4094 tpnz 4096 onn0 5490 oawordeulem 7260 noinfep 8170 fin23lem31 8778 isfin1-3 8821 omina 9121 rpnnen1lem4 11300 rpnnen1lem5 11301 rexfiuz 13422 caurcvg 13754 caurcvgOLD 13755 caurcvg2 13756 caucvg 13757 infcvgaux1i 13927 divalglem2 14385 divalglem2OLD 14386 pc2dvds 14840 vdwmc2 14941 cnsubglem 19029 cnmsubglem 19042 pmatcollpw3 19820 zfbas 20923 nrginvrcn 21706 lebnumlem3 22003 lebnumlem3OLD 22006 caun0 22263 cnflduss 22335 cnfldcusp 22336 reust 22352 recusp 22353 nulmbl2 22502 itg2seq 22712 itg2monolem1 22720 c1lip1 22961 aannenlem2 23297 logbmpt 23737 tgcgr4 24588 shintcl 26995 chintcl 26997 nmoprepnf 27532 nmfnrepnf 27545 nmcexi 27691 snct 28307 esum0 28882 esumpcvgval 28911 bnj906 29753 bj-tagn0 31585 taupi 31736 ismblfin 31993 volsupnfl 31997 itg2addnclem 32005 ftc1anc 32037 incsequz 32089 isbnd3 32128 ssbnd 32132 corclrcl 36311 imo72b2lem0 36620 imo72b2lem2 36622 imo72b2lem1 36626 imo72b2 36630 amgm2d 36661 ioodvbdlimc1 37817 ioodvbdlimc2 37820 dvnprodlem3 37833 stirlinglem13 37958 fourierdlem103 38083 fourierdlem104 38084 fouriersw 38105 hoicvr 38380 2zlidl 40038 |
Copyright terms: Public domain | W3C validator |