Theorem ne0ii 4297

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

Syntax hints:   ∈ wcel 2109   ≠ wne 2925  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-dif 3908  df-nul 4287

This theorem is referenced by:  vn0ALT  4299  prnz  4731  tpnz  4733  pwne0  5299  onn0  6377  oawordeulem  8479  noinfep  9575  fin23lem31  10256  isfin1-3  10299  omina  10604  nnunb  12398  rpnnen1lem4  12899  rpnnen1lem5  12900  rexfiuz  15273  caurcvg  15602  caurcvg2  15603  caucvg  15604  infcvgaux1i  15782  divalglem2  16324  pc2dvds  16809  vdwmc2  16909  cnsubglem  21340  cnmsubglem  21355  pzriprnglem4  21409  pmatcollpw3  22687  zfbas  23799  nrginvrcn  24596  lebnumlem3  24878  caun0  25197  cnflduss  25272  cnfldcusp  25273  reust  25297  recusp  25298  nulmbl2  25453  itg2seq  25659  itg2monolem1  25667  c1lip1  25918  aannenlem2  26253  logbmpt  26714  tgcgr4  28494  shintcl  31292  chintcl  31294  nmoprepnf  31829  nmfnrepnf  31842  nmcexi  31988  snct  32670  constrext2chnlem  33719  constrfiss  33720  esum0  34018  esumpcvgval  34047  bnj906  34899  satf0  35347  fmla1  35362  prv0  35405  bj-tagn0  36955  taupi  37299  ismblfin  37643  volsupnfl  37647  itg2addnclem  37653  ftc1anc  37683  incsequz  37730  isbnd3  37766  ssbnd  37770  onexomgt  43217  dflim5  43305  corclrcl  43683  imo72b2lem2  44143  imo72b2lem1  44145  imo72b2  44148  amgm2d  44174  nnn0  45361  ren0  45385  ioodvbdlimc1  45918  ioodvbdlimc2  45920  stirlinglem13  46071  fourierdlem103  46194  fourierdlem104  46195  fouriersw  46216  hoicvr  46533  2zlidl  48228  termc2  49507