Theorem ne0ii 4298

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

Syntax hints:   ∈ wcel 2114   ≠ wne 2933  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3906  df-nul 4288

This theorem is referenced by:  vn0ALT  4300  prnz  4736  tpnz  4738  pwne0  5304  onn0  6391  oawordeulem  8491  noinfep  9581  fin23lem31  10265  isfin1-3  10308  omina  10614  nnunb  12409  rpnnen1lem4  12905  rpnnen1lem5  12906  rexfiuz  15283  caurcvg  15612  caurcvg2  15613  caucvg  15614  infcvgaux1i  15792  divalglem2  16334  pc2dvds  16819  vdwmc2  16919  cnsubglem  21382  cnmsubglem  21397  pzriprnglem4  21451  pmatcollpw3  22740  zfbas  23852  nrginvrcn  24648  lebnumlem3  24930  caun0  25249  cnflduss  25324  cnfldcusp  25325  reust  25349  recusp  25350  nulmbl2  25505  itg2seq  25711  itg2monolem1  25719  c1lip1  25970  aannenlem2  26305  logbmpt  26766  tgcgr4  28615  shintcl  31417  chintcl  31419  nmoprepnf  31954  nmfnrepnf  31967  nmcexi  32113  snct  32801  constrext2chnlem  33927  constrfiss  33928  esum0  34226  esumpcvgval  34255  bnj906  35105  satf0  35585  fmla1  35600  prv0  35643  bj-tagn0  37224  taupi  37575  ismblfin  37909  volsupnfl  37913  itg2addnclem  37919  ftc1anc  37949  incsequz  37996  isbnd3  38032  ssbnd  38036  onexomgt  43595  dflim5  43683  corclrcl  44060  imo72b2lem2  44520  imo72b2lem1  44522  imo72b2  44525  amgm2d  44551  nnn0  45733  ren0  45757  ioodvbdlimc1  46288  ioodvbdlimc2  46290  stirlinglem13  46441  fourierdlem103  46564  fourierdlem104  46565  fouriersw  46586  hoicvr  46903  2zlidl  48597  termc2  49874