Theorem ne0ii 4337

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

Syntax hints:   ∈ wcel 2105   ≠ wne 2939  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-dif 3951  df-nul 4323

This theorem is referenced by:  vn0ALT  4339  prnz  4781  tpnz  4783  pwne0  5355  onn0  6429  oawordeulem  8560  noinfep  9661  fin23lem31  10344  isfin1-3  10387  omina  10692  nnunb  12475  rpnnen1lem4  12971  rpnnen1lem5  12972  rexfiuz  15301  caurcvg  15630  caurcvg2  15631  caucvg  15632  infcvgaux1i  15810  divalglem2  16345  pc2dvds  16819  vdwmc2  16919  cnsubglem  21283  cnmsubglem  21297  pzriprnglem4  21344  pmatcollpw3  22606  zfbas  23720  nrginvrcn  24529  lebnumlem3  24809  caun0  25129  cnflduss  25204  cnfldcusp  25205  reust  25229  recusp  25230  nulmbl2  25385  itg2seq  25592  itg2monolem1  25600  c1lip1  25850  aannenlem2  26181  logbmpt  26634  tgcgr4  28216  shintcl  31017  chintcl  31019  nmoprepnf  31554  nmfnrepnf  31567  nmcexi  31713  snct  32372  esum0  33512  esumpcvgval  33541  bnj906  34406  satf0  34828  fmla1  34843  prv0  34886  bj-tagn0  36326  taupi  36670  ismblfin  36995  volsupnfl  36999  itg2addnclem  37005  ftc1anc  37035  incsequz  37082  isbnd3  37118  ssbnd  37122  onexomgt  42455  dflim5  42544  corclrcl  42923  imo72b2lem0  43382  imo72b2lem2  43384  imo72b2lem1  43386  imo72b2  43389  amgm2d  43415  nnn0  44549  ren0  44573  ioodvbdlimc1  45110  ioodvbdlimc2  45112  stirlinglem13  45263  fourierdlem103  45386  fourierdlem104  45387  fouriersw  45408  hoicvr  45725  2zlidl  47079