Theorem ne0ii 4350

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

Syntax hints:   ∈ wcel 2106   ≠ wne 2938  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-dif 3966  df-nul 4340

This theorem is referenced by:  vn0ALT  4352  prnz  4782  tpnz  4784  pwne0  5363  onn0  6451  oawordeulem  8591  noinfep  9698  fin23lem31  10381  isfin1-3  10424  omina  10729  nnunb  12520  rpnnen1lem4  13020  rpnnen1lem5  13021  rexfiuz  15383  caurcvg  15710  caurcvg2  15711  caucvg  15712  infcvgaux1i  15890  divalglem2  16429  pc2dvds  16913  vdwmc2  17013  cnsubglem  21451  cnmsubglem  21466  pzriprnglem4  21513  pmatcollpw3  22806  zfbas  23920  nrginvrcn  24729  lebnumlem3  25009  caun0  25329  cnflduss  25404  cnfldcusp  25405  reust  25429  recusp  25430  nulmbl2  25585  itg2seq  25792  itg2monolem1  25800  c1lip1  26051  aannenlem2  26386  logbmpt  26846  tgcgr4  28554  shintcl  31359  chintcl  31361  nmoprepnf  31896  nmfnrepnf  31909  nmcexi  32055  snct  32731  esum0  34030  esumpcvgval  34059  bnj906  34923  satf0  35357  fmla1  35372  prv0  35415  bj-tagn0  36962  taupi  37306  ismblfin  37648  volsupnfl  37652  itg2addnclem  37658  ftc1anc  37688  incsequz  37735  isbnd3  37771  ssbnd  37775  onexomgt  43230  dflim5  43319  corclrcl  43697  imo72b2lem2  44157  imo72b2lem1  44159  imo72b2  44162  amgm2d  44188  nnn0  45328  ren0  45352  ioodvbdlimc1  45889  ioodvbdlimc2  45891  stirlinglem13  46042  fourierdlem103  46165  fourierdlem104  46166  fouriersw  46187  hoicvr  46504  2zlidl  48084