![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ne0ii | Structured version Visualization version GIF version |
Description: If a class has elements, then it is nonempty. Inference associated with ne0i 4120. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
n0ii.1 | ⊢ 𝐴 ∈ 𝐵 |
Ref | Expression |
---|---|
ne0ii | ⊢ 𝐵 ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0ii.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | ne0i 4120 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 ≠ wne 2970 ∅c0 4114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2776 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ne 2971 df-v 3386 df-dif 3771 df-nul 4115 |
This theorem is referenced by: vn0 4124 prnz 4497 tpnz 4499 pwne0 5026 onn0 6004 oawordeulem 7873 noinfep 8806 fin23lem31 9452 isfin1-3 9495 omina 9800 rpnnen1lem4 12061 rpnnen1lem5 12062 rexfiuz 14425 caurcvg 14745 caurcvg2 14746 caucvg 14747 infcvgaux1i 14924 divalglem2 15451 pc2dvds 15913 vdwmc2 16013 cnsubglem 20114 cnmsubglem 20128 pmatcollpw3 20914 zfbas 22025 nrginvrcn 22821 lebnumlem3 23087 caun0 23404 cnflduss 23479 cnfldcusp 23480 reust 23504 recusp 23505 nulmbl2 23641 itg2seq 23847 itg2monolem1 23855 c1lip1 24098 aannenlem2 24422 logbmpt 24867 tgcgr4 25775 shintcl 28707 chintcl 28709 nmoprepnf 29244 nmfnrepnf 29257 nmcexi 29403 snct 30002 esum0 30620 esumpcvgval 30649 bnj906 31510 bj-tagn0 33452 taupi 33661 ismblfin 33932 volsupnfl 33936 itg2addnclem 33942 ftc1anc 33974 incsequz 34024 isbnd3 34063 ssbnd 34067 corclrcl 38771 imo72b2lem0 39236 imo72b2lem2 39238 imo72b2lem1 39242 imo72b2 39246 amgm2d 39272 nnn0 40328 ren0 40358 ioodvbdlimc1 40881 ioodvbdlimc2 40883 stirlinglem13 41035 fourierdlem103 41158 fourierdlem104 41159 fouriersw 41180 hoicvr 41497 2zlidl 42722 |
Copyright terms: Public domain | W3C validator |