Theorem ne0ii 4284

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

Syntax hints:   ∈ wcel 2114   ≠ wne 2932  ∅c0 4273

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3892  df-nul 4274

This theorem is referenced by:  vn0ALT  4286  prnz  4721  tpnz  4723  pwne0  5298  onn0  6389  oawordeulem  8489  noinfep  9581  fin23lem31  10265  isfin1-3  10308  omina  10614  nnunb  12433  rpnnen1lem4  12930  rpnnen1lem5  12931  rexfiuz  15310  caurcvg  15639  caurcvg2  15640  caucvg  15641  infcvgaux1i  15822  divalglem2  16364  pc2dvds  16850  vdwmc2  16950  cnsubglem  21396  cnmsubglem  21410  pzriprnglem4  21464  pmatcollpw3  22749  zfbas  23861  nrginvrcn  24657  lebnumlem3  24930  caun0  25248  cnflduss  25323  cnfldcusp  25324  reust  25348  recusp  25349  nulmbl2  25503  itg2seq  25709  itg2monolem1  25717  c1lip1  25964  aannenlem2  26295  logbmpt  26752  tgcgr4  28599  shintcl  31401  chintcl  31403  nmoprepnf  31938  nmfnrepnf  31951  nmcexi  32097  snct  32785  constrext2chnlem  33894  constrfiss  33895  esum0  34193  esumpcvgval  34222  bnj906  35072  satf0  35554  fmla1  35569  prv0  35612  bj-tagn0  37286  taupi  37637  ismblfin  37982  volsupnfl  37986  itg2addnclem  37992  ftc1anc  38022  incsequz  38069  isbnd3  38105  ssbnd  38109  onexomgt  43669  dflim5  43757  corclrcl  44134  imo72b2lem2  44594  imo72b2lem1  44596  imo72b2  44599  amgm2d  44625  nnn0  45807  ren0  45830  ioodvbdlimc1  46361  ioodvbdlimc2  46363  stirlinglem13  46514  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  2zlidl  48716  termc2  49993