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 4223. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
n0ii.1 | ⊢ 𝐴 ∈ 𝐵 |
Ref | Expression |
---|---|
ne0ii | ⊢ 𝐵 ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0ii.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | ne0i 4223 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 ≠ wne 2934 ∅c0 4211 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ne 2935 df-dif 3846 df-nul 4212 |
This theorem is referenced by: vn0ALT 4228 prnz 4668 tpnz 4670 pwne0 5223 onn0 6236 oawordeulem 8213 noinfep 9198 fin23lem31 9845 isfin1-3 9888 omina 10193 nnunb 11974 rpnnen1lem4 12464 rpnnen1lem5 12465 rexfiuz 14799 caurcvg 15128 caurcvg2 15129 caucvg 15130 infcvgaux1i 15307 divalglem2 15842 pc2dvds 16317 vdwmc2 16417 cnsubglem 20268 cnmsubglem 20282 pmatcollpw3 21537 zfbas 22649 nrginvrcn 23447 lebnumlem3 23717 caun0 24035 cnflduss 24110 cnfldcusp 24111 reust 24135 recusp 24136 nulmbl2 24290 itg2seq 24497 itg2monolem1 24505 c1lip1 24751 aannenlem2 25079 logbmpt 25528 tgcgr4 26479 shintcl 29267 chintcl 29269 nmoprepnf 29804 nmfnrepnf 29817 nmcexi 29963 snct 30625 esum0 31589 esumpcvgval 31618 bnj906 32483 satf0 32907 fmla1 32922 prv0 32965 bj-tagn0 34814 taupi 35136 ismblfin 35463 volsupnfl 35467 itg2addnclem 35473 ftc1anc 35503 incsequz 35551 isbnd3 35587 ssbnd 35591 corclrcl 40883 imo72b2lem0 41344 imo72b2lem2 41346 imo72b2lem1 41348 imo72b2 41352 amgm2d 41378 nnn0 42477 ren0 42502 ioodvbdlimc1 43038 ioodvbdlimc2 43040 stirlinglem13 43191 fourierdlem103 43314 fourierdlem104 43315 fouriersw 43336 hoicvr 43650 2zlidl 45055 |
Copyright terms: Public domain | W3C validator |