Theorem ne0ii 4302

Description: If a class has elements, then it is nonempty. Inference associated with ne0i 4299. (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 4299	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐵 ≠ ∅)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 ≠ ∅

Syntax hints:   ∈ wcel 2106   ≠ wne 2939  ∅c0 4287

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-dif 3916  df-nul 4288

This theorem is referenced by:  vn0ALT  4304  prnz  4743  tpnz  4745  pwne0  5317  onn0  6387  oawordeulem  8506  noinfep  9605  fin23lem31  10288  isfin1-3  10331  omina  10636  nnunb  12418  rpnnen1lem4  12914  rpnnen1lem5  12915  rexfiuz  15244  caurcvg  15573  caurcvg2  15574  caucvg  15575  infcvgaux1i  15753  divalglem2  16288  pc2dvds  16762  vdwmc2  16862  cnsubglem  20883  cnmsubglem  20897  pmatcollpw3  22170  zfbas  23284  nrginvrcn  24093  lebnumlem3  24363  caun0  24682  cnflduss  24757  cnfldcusp  24758  reust  24782  recusp  24783  nulmbl2  24937  itg2seq  25144  itg2monolem1  25152  c1lip1  25398  aannenlem2  25726  logbmpt  26175  tgcgr4  27536  shintcl  30335  chintcl  30337  nmoprepnf  30872  nmfnrepnf  30885  nmcexi  31031  snct  31698  esum0  32737  esumpcvgval  32766  bnj906  33631  satf0  34053  fmla1  34068  prv0  34111  bj-tagn0  35523  taupi  35867  ismblfin  36192  volsupnfl  36196  itg2addnclem  36202  ftc1anc  36232  incsequz  36280  isbnd3  36316  ssbnd  36320  onexomgt  41633  dflim5  41722  corclrcl  42101  imo72b2lem0  42560  imo72b2lem2  42562  imo72b2lem1  42564  imo72b2  42567  amgm2d  42593  nnn0  43733  ren0  43757  ioodvbdlimc1  44294  ioodvbdlimc2  44296  stirlinglem13  44447  fourierdlem103  44570  fourierdlem104  44571  fouriersw  44592  hoicvr  44909  2zlidl  46352