Theorem ne0ii 4301

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

Syntax hints:   ∈ wcel 2108   ≠ wne 3014  ∅c0 4289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-ne 3015  df-dif 3937  df-nul 4290

This theorem is referenced by:  vn0  4302  prnz  4704  tpnz  4706  pwne0  5248  onn0  6248  oawordeulem  8172  noinfep  9115  fin23lem31  9757  isfin1-3  9800  omina  10105  nnunb  11885  rpnnen1lem4  12371  rpnnen1lem5  12372  rexfiuz  14699  caurcvg  15025  caurcvg2  15026  caucvg  15027  infcvgaux1i  15204  divalglem2  15738  pc2dvds  16207  vdwmc2  16307  cnsubglem  20586  cnmsubglem  20600  pmatcollpw3  21384  zfbas  22496  nrginvrcn  23293  lebnumlem3  23559  caun0  23876  cnflduss  23951  cnfldcusp  23952  reust  23976  recusp  23977  nulmbl2  24129  itg2seq  24335  itg2monolem1  24343  c1lip1  24586  aannenlem2  24910  logbmpt  25358  tgcgr4  26309  shintcl  29099  chintcl  29101  nmoprepnf  29636  nmfnrepnf  29649  nmcexi  29795  snct  30441  esum0  31301  esumpcvgval  31330  bnj906  32195  satf0  32612  fmla1  32627  prv0  32670  bj-tagn0  34284  taupi  34596  ismblfin  34925  volsupnfl  34929  itg2addnclem  34935  ftc1anc  34967  incsequz  35015  isbnd3  35054  ssbnd  35058  corclrcl  40042  imo72b2lem0  40506  imo72b2lem2  40508  imo72b2lem1  40511  imo72b2  40515  amgm2d  40541  nnn0  41636  ren0  41664  ioodvbdlimc1  42207  ioodvbdlimc2  42209  stirlinglem13  42361  fourierdlem103  42484  fourierdlem104  42485  fouriersw  42506  hoicvr  42820  2zlidl  44195