Theorem ne0ii 4338

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

Syntax hints:   ∈ wcel 2107   ≠ wne 2941  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-dif 3952  df-nul 4324

This theorem is referenced by:  vn0ALT  4340  prnz  4782  tpnz  4784  pwne0  5356  onn0  6430  oawordeulem  8554  noinfep  9655  fin23lem31  10338  isfin1-3  10381  omina  10686  nnunb  12468  rpnnen1lem4  12964  rpnnen1lem5  12965  rexfiuz  15294  caurcvg  15623  caurcvg2  15624  caucvg  15625  infcvgaux1i  15803  divalglem2  16338  pc2dvds  16812  vdwmc2  16912  cnsubglem  20994  cnmsubglem  21008  pmatcollpw3  22286  zfbas  23400  nrginvrcn  24209  lebnumlem3  24479  caun0  24798  cnflduss  24873  cnfldcusp  24874  reust  24898  recusp  24899  nulmbl2  25053  itg2seq  25260  itg2monolem1  25268  c1lip1  25514  aannenlem2  25842  logbmpt  26293  tgcgr4  27782  shintcl  30583  chintcl  30585  nmoprepnf  31120  nmfnrepnf  31133  nmcexi  31279  snct  31938  esum0  33047  esumpcvgval  33076  bnj906  33941  satf0  34363  fmla1  34378  prv0  34421  bj-tagn0  35860  taupi  36204  ismblfin  36529  volsupnfl  36533  itg2addnclem  36539  ftc1anc  36569  incsequz  36616  isbnd3  36652  ssbnd  36656  onexomgt  41990  dflim5  42079  corclrcl  42458  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2lem1  42921  imo72b2  42924  amgm2d  42950  nnn0  44088  ren0  44112  ioodvbdlimc1  44649  ioodvbdlimc2  44651  stirlinglem13  44802  fourierdlem103  44925  fourierdlem104  44926  fouriersw  44947  hoicvr  45264  pzriprnglem4  46808  2zlidl  46832