Theorem ne0ii 4268

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2942  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-dif 3886  df-nul 4254

This theorem is referenced by:  vn0ALT  4270  prnz  4710  tpnz  4712  pwne0  5274  onn0  6315  oawordeulem  8347  noinfep  9348  fin23lem31  10030  isfin1-3  10073  omina  10378  nnunb  12159  rpnnen1lem4  12649  rpnnen1lem5  12650  rexfiuz  14987  caurcvg  15316  caurcvg2  15317  caucvg  15318  infcvgaux1i  15497  divalglem2  16032  pc2dvds  16508  vdwmc2  16608  cnsubglem  20559  cnmsubglem  20573  pmatcollpw3  21841  zfbas  22955  nrginvrcn  23762  lebnumlem3  24032  caun0  24350  cnflduss  24425  cnfldcusp  24426  reust  24450  recusp  24451  nulmbl2  24605  itg2seq  24812  itg2monolem1  24820  c1lip1  25066  aannenlem2  25394  logbmpt  25843  tgcgr4  26796  shintcl  29593  chintcl  29595  nmoprepnf  30130  nmfnrepnf  30143  nmcexi  30289  snct  30950  esum0  31917  esumpcvgval  31946  bnj906  32810  satf0  33234  fmla1  33249  prv0  33292  bj-tagn0  35096  taupi  35421  ismblfin  35745  volsupnfl  35749  itg2addnclem  35755  ftc1anc  35785  incsequz  35833  isbnd3  35869  ssbnd  35873  corclrcl  41204  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2lem1  41669  imo72b2  41672  amgm2d  41698  nnn0  42807  ren0  42832  ioodvbdlimc1  43364  ioodvbdlimc2  43366  stirlinglem13  43517  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  hoicvr  43976  2zlidl  45380