Theorem ne0ii 4290

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

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2956  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3902  df-nul 4280

This theorem is used by:  vn0ALT  4293  prnz  4738  tpnz  4740  pwne0  5318  onn0  6422  oawordeulem  8546  noinfep  9645  fin23lem31  10402  isfin1-3  10445  omina  10757  nnunb  12583  rpnnen1lem4  13089  rpnnen1lem5  13090  rexfiuz  15495  caurcvg  15824  caurcvg2  15825  caucvg  15826  infcvgaux1i  16006  divalglem2  16545  pc2dvds  17037  vdwmc2  17137  cnsubglem  21702  cnmsubglem  21716  pzriprnglem4  21770  pmatcollpw3  23082  zfbas  24195  nrginvrcn  24991  lebnumlem3  25264  caun0  25582  cnflduss  25657  cnfldcusp  25658  reust  25682  recusp  25683  nulmbl2  25837  itg2seq  26043  itg2monolem1  26051  c1lip1  26297  aannenlem2  26638  logbmpt  27098  tgcgr4  28976  shintcl  31914  chintcl  31916  nmoprepnf  32451  nmfnrepnf  32464  nmcexi  32610  snct  33287  constrext2chnlem  34364  constrfiss  34365  esum0  34663  esumpcvgval  34692  bnj906  35543  satf0  36106  fmla1  36121  prv0  36164  bj-tagn0  37862  taupi  38212  ismblfin  38547  volsupnfl  38551  itg2addnclem  38557  ftc1anc  38587  incsequz  38650  isbnd3  38686  ssbnd  38690  onexomgt  44201  dflim5  44289  corclrcl  44666  imo72b2lem2  45126  imo72b2lem1  45128  imo72b2  45131  amgm2d  45157  nnn0  46333  ren0  46356  ioodvbdlimc1  46887  ioodvbdlimc2  46889  stirlinglem13  47040  fourierdlem103  47163  fourierdlem104  47164  fouriersw  47185  2zlidl  49281  termc2  50570  veronesematrowd  50925  veroquadmodzerod  50928  veroquadnolindfd  50929