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 4269. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
n0ii.1 | ⊢ 𝐴 ∈ 𝐵 |
Ref | Expression |
---|---|
ne0ii | ⊢ 𝐵 ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0ii.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | ne0i 4269 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ≠ wne 2944 ∅c0 4257 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-ne 2945 df-dif 3891 df-nul 4258 |
This theorem is referenced by: vn0ALT 4274 prnz 4714 tpnz 4716 pwne0 5280 onn0 6334 oawordeulem 8394 noinfep 9427 fin23lem31 10108 isfin1-3 10151 omina 10456 nnunb 12238 rpnnen1lem4 12729 rpnnen1lem5 12730 rexfiuz 15068 caurcvg 15397 caurcvg2 15398 caucvg 15399 infcvgaux1i 15578 divalglem2 16113 pc2dvds 16589 vdwmc2 16689 cnsubglem 20656 cnmsubglem 20670 pmatcollpw3 21942 zfbas 23056 nrginvrcn 23865 lebnumlem3 24135 caun0 24454 cnflduss 24529 cnfldcusp 24530 reust 24554 recusp 24555 nulmbl2 24709 itg2seq 24916 itg2monolem1 24924 c1lip1 25170 aannenlem2 25498 logbmpt 25947 tgcgr4 26901 shintcl 29701 chintcl 29703 nmoprepnf 30238 nmfnrepnf 30251 nmcexi 30397 snct 31057 esum0 32026 esumpcvgval 32055 bnj906 32919 satf0 33343 fmla1 33358 prv0 33401 bj-tagn0 35178 taupi 35503 ismblfin 35827 volsupnfl 35831 itg2addnclem 35837 ftc1anc 35867 incsequz 35915 isbnd3 35951 ssbnd 35955 corclrcl 41322 imo72b2lem0 41783 imo72b2lem2 41785 imo72b2lem1 41787 imo72b2 41790 amgm2d 41816 nnn0 42924 ren0 42949 ioodvbdlimc1 43481 ioodvbdlimc2 43483 stirlinglem13 43634 fourierdlem103 43757 fourierdlem104 43758 fouriersw 43779 hoicvr 44093 2zlidl 45503 |
Copyright terms: Public domain | W3C validator |