Theorem ne0ii 4307

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

Syntax hints:   ∈ wcel 2109   ≠ wne 2925  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-dif 3917  df-nul 4297

This theorem is referenced by:  vn0ALT  4309  prnz  4741  tpnz  4743  pwne0  5312  onn0  6398  oawordeulem  8518  noinfep  9613  fin23lem31  10296  isfin1-3  10339  omina  10644  nnunb  12438  rpnnen1lem4  12939  rpnnen1lem5  12940  rexfiuz  15314  caurcvg  15643  caurcvg2  15644  caucvg  15645  infcvgaux1i  15823  divalglem2  16365  pc2dvds  16850  vdwmc2  16950  cnsubglem  21332  cnmsubglem  21347  pzriprnglem4  21394  pmatcollpw3  22671  zfbas  23783  nrginvrcn  24580  lebnumlem3  24862  caun0  25181  cnflduss  25256  cnfldcusp  25257  reust  25281  recusp  25282  nulmbl2  25437  itg2seq  25643  itg2monolem1  25651  c1lip1  25902  aannenlem2  26237  logbmpt  26698  tgcgr4  28458  shintcl  31259  chintcl  31261  nmoprepnf  31796  nmfnrepnf  31809  nmcexi  31955  snct  32637  constrext2chnlem  33740  constrfiss  33741  esum0  34039  esumpcvgval  34068  bnj906  34920  satf0  35359  fmla1  35374  prv0  35417  bj-tagn0  36967  taupi  37311  ismblfin  37655  volsupnfl  37659  itg2addnclem  37665  ftc1anc  37695  incsequz  37742  isbnd3  37778  ssbnd  37782  onexomgt  43230  dflim5  43318  corclrcl  43696  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  amgm2d  44187  nnn0  45374  ren0  45398  ioodvbdlimc1  45931  ioodvbdlimc2  45933  stirlinglem13  46084  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  hoicvr  46546  2zlidl  48228  termc2  49507