Theorem ne0ii 4299

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

Syntax hints:   ∈ wcel 2145   ≠ wne 2960  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3910  df-nul 4289

This theorem is referenced by:  vn0ALT  4301  prnz  4739  tpnz  4741  pwne0  5318  onn0  6416  oawordeulem  8527  noinfep  9617  fin23lem31  10315  isfin1-3  10358  omina  10664  nnunb  12491  rpnnen1lem4  12995  rpnnen1lem5  12996  rexfiuz  15389  caurcvg  15718  caurcvg2  15719  caucvg  15720  infcvgaux1i  15901  divalglem2  16443  pc2dvds  16929  vdwmc2  17029  cnsubglem  21526  cnmsubglem  21540  pzriprnglem4  21594  pmatcollpw3  22902  zfbas  24014  nrginvrcn  24810  lebnumlem3  25083  caun0  25401  cnflduss  25476  cnfldcusp  25477  reust  25501  recusp  25502  nulmbl2  25656  itg2seq  25862  itg2monolem1  25870  c1lip1  26117  aannenlem2  26451  logbmpt  26911  tgcgr4  28758  shintcl  31591  chintcl  31593  nmoprepnf  32128  nmfnrepnf  32141  nmcexi  32287  snct  32969  constrext2chnlem  34057  constrfiss  34058  esum0  34356  esumpcvgval  34385  bnj906  35235  satf0  35735  fmla1  35750  prv0  35793  bj-tagn0  37476  taupi  37827  ismblfin  38172  volsupnfl  38176  itg2addnclem  38182  ftc1anc  38212  incsequz  38259  isbnd3  38295  ssbnd  38299  onexomgt  43830  dflim5  43918  corclrcl  44295  imo72b2lem2  44755  imo72b2lem1  44757  imo72b2  44760  amgm2d  44786  nnn0  45951  ren0  45974  ioodvbdlimc1  46505  ioodvbdlimc2  46507  stirlinglem13  46658  fourierdlem103  46781  fourierdlem104  46782  fouriersw  46803  2zlidl  48860  termc2  50147