Theorem ne0ii 4253

Description: If a class has elements, then it is nonempty. Inference associated with ne0i 4250. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
n0ii.1	⊢ 𝐴 ∈ 𝐵

Assertion

Ref	Expression
ne0ii	⊢ 𝐵 ≠ ∅

Proof of Theorem ne0ii

Step	Hyp	Ref	Expression
1		n0ii.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		ne0i 4250	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 ≠ ∅

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