| 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 4341. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| Ref | Expression |
|---|---|
| n0ii.1 | ⊢ 𝐴 ∈ 𝐵 |
| Ref | Expression |
|---|---|
| ne0ii | ⊢ 𝐵 ≠ ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | n0ii.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
| 2 | ne0i 4341 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≠ ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 ≠ wne 2940 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: vn0ALT 4346 prnz 4777 tpnz 4779 pwne0 5357 onn0 6449 oawordeulem 8592 noinfep 9700 fin23lem31 10383 isfin1-3 10426 omina 10731 nnunb 12522 rpnnen1lem4 13022 rpnnen1lem5 13023 rexfiuz 15386 caurcvg 15713 caurcvg2 15714 caucvg 15715 infcvgaux1i 15893 divalglem2 16432 pc2dvds 16917 vdwmc2 17017 cnsubglem 21433 cnmsubglem 21448 pzriprnglem4 21495 pmatcollpw3 22790 zfbas 23904 nrginvrcn 24713 lebnumlem3 24995 caun0 25315 cnflduss 25390 cnfldcusp 25391 reust 25415 recusp 25416 nulmbl2 25571 itg2seq 25777 itg2monolem1 25785 c1lip1 26036 aannenlem2 26371 logbmpt 26831 tgcgr4 28539 shintcl 31349 chintcl 31351 nmoprepnf 31886 nmfnrepnf 31899 nmcexi 32045 snct 32725 esum0 34050 esumpcvgval 34079 bnj906 34944 satf0 35377 fmla1 35392 prv0 35435 bj-tagn0 36980 taupi 37324 ismblfin 37668 volsupnfl 37672 itg2addnclem 37678 ftc1anc 37708 incsequz 37755 isbnd3 37791 ssbnd 37795 onexomgt 43253 dflim5 43342 corclrcl 43720 imo72b2lem2 44180 imo72b2lem1 44182 imo72b2 44185 amgm2d 44211 nnn0 45389 ren0 45413 ioodvbdlimc1 45948 ioodvbdlimc2 45950 stirlinglem13 46101 fourierdlem103 46224 fourierdlem104 46225 fouriersw 46246 hoicvr 46563 2zlidl 48156 termc2 49148 |
| Copyright terms: Public domain | W3C validator |