![]() |
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 4250. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
n0ii.1 | ⊢ 𝐴 ∈ 𝐵 |
Ref | Expression |
---|---|
ne0ii | ⊢ 𝐵 ≠ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0ii.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | ne0i 4250 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 ≠ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 ≠ wne 2987 ∅c0 4243 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ne 2988 df-dif 3884 df-nul 4244 |
This theorem is referenced by: vn0 4254 prnz 4673 tpnz 4675 pwne0 5222 onn0 6223 oawordeulem 8163 noinfep 9107 fin23lem31 9754 isfin1-3 9797 omina 10102 nnunb 11881 rpnnen1lem4 12367 rpnnen1lem5 12368 rexfiuz 14699 caurcvg 15025 caurcvg2 15026 caucvg 15027 infcvgaux1i 15204 divalglem2 15736 pc2dvds 16205 vdwmc2 16305 cnsubglem 20140 cnmsubglem 20154 pmatcollpw3 21389 zfbas 22501 nrginvrcn 23298 lebnumlem3 23568 caun0 23885 cnflduss 23960 cnfldcusp 23961 reust 23985 recusp 23986 nulmbl2 24140 itg2seq 24346 itg2monolem1 24354 c1lip1 24600 aannenlem2 24925 logbmpt 25374 tgcgr4 26325 shintcl 29113 chintcl 29115 nmoprepnf 29650 nmfnrepnf 29663 nmcexi 29809 snct 30475 esum0 31418 esumpcvgval 31447 bnj906 32312 satf0 32732 fmla1 32747 prv0 32790 bj-tagn0 34415 taupi 34737 ismblfin 35098 volsupnfl 35102 itg2addnclem 35108 ftc1anc 35138 incsequz 35186 isbnd3 35222 ssbnd 35226 corclrcl 40408 imo72b2lem0 40869 imo72b2lem2 40871 imo72b2lem1 40874 imo72b2 40878 amgm2d 40904 nnn0 42011 ren0 42039 ioodvbdlimc1 42575 ioodvbdlimc2 42577 stirlinglem13 42728 fourierdlem103 42851 fourierdlem104 42852 fouriersw 42873 hoicvr 43187 2zlidl 44558 |
Copyright terms: Public domain | W3C validator |