Theorem ne0ii 4305

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

Syntax hints:   ∈ wcel 2114   ≠ wne 3018  ∅c0 4293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ne 3019  df-dif 3941  df-nul 4294

This theorem is referenced by:  vn0  4306  prnz  4714  tpnz  4716  pwne0  5259  onn0  6257  oawordeulem  8182  noinfep  9125  fin23lem31  9767  isfin1-3  9810  omina  10115  nnunb  11896  rpnnen1lem4  12382  rpnnen1lem5  12383  rexfiuz  14709  caurcvg  15035  caurcvg2  15036  caucvg  15037  infcvgaux1i  15214  divalglem2  15748  pc2dvds  16217  vdwmc2  16317  cnsubglem  20596  cnmsubglem  20610  pmatcollpw3  21394  zfbas  22506  nrginvrcn  23303  lebnumlem3  23569  caun0  23886  cnflduss  23961  cnfldcusp  23962  reust  23986  recusp  23987  nulmbl2  24139  itg2seq  24345  itg2monolem1  24353  c1lip1  24596  aannenlem2  24920  logbmpt  25368  tgcgr4  26319  shintcl  29109  chintcl  29111  nmoprepnf  29646  nmfnrepnf  29659  nmcexi  29805  snct  30451  esum0  31310  esumpcvgval  31339  bnj906  32204  satf0  32621  fmla1  32636  prv0  32679  bj-tagn0  34293  taupi  34606  ismblfin  34935  volsupnfl  34939  itg2addnclem  34945  ftc1anc  34977  incsequz  35025  isbnd3  35064  ssbnd  35068  corclrcl  40059  imo72b2lem0  40523  imo72b2lem2  40525  imo72b2lem1  40528  imo72b2  40532  amgm2d  40558  nnn0  41654  ren0  41682  ioodvbdlimc1  42225  ioodvbdlimc2  42227  stirlinglem13  42378  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  hoicvr  42837  2zlidl  44212