Theorem ne0ii 4319

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2932  ∅c0 4308

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-dif 3929  df-nul 4309

This theorem is referenced by:  vn0ALT  4321  prnz  4753  tpnz  4755  pwne0  5327  onn0  6418  oawordeulem  8566  noinfep  9674  fin23lem31  10357  isfin1-3  10400  omina  10705  nnunb  12497  rpnnen1lem4  12996  rpnnen1lem5  12997  rexfiuz  15366  caurcvg  15693  caurcvg2  15694  caucvg  15695  infcvgaux1i  15873  divalglem2  16414  pc2dvds  16899  vdwmc2  16999  cnsubglem  21383  cnmsubglem  21398  pzriprnglem4  21445  pmatcollpw3  22722  zfbas  23834  nrginvrcn  24631  lebnumlem3  24913  caun0  25233  cnflduss  25308  cnfldcusp  25309  reust  25333  recusp  25334  nulmbl2  25489  itg2seq  25695  itg2monolem1  25703  c1lip1  25954  aannenlem2  26289  logbmpt  26750  tgcgr4  28510  shintcl  31311  chintcl  31313  nmoprepnf  31848  nmfnrepnf  31861  nmcexi  32007  snct  32691  constrext2chnlem  33784  constrfiss  33785  esum0  34080  esumpcvgval  34109  bnj906  34961  satf0  35394  fmla1  35409  prv0  35452  bj-tagn0  36997  taupi  37341  ismblfin  37685  volsupnfl  37689  itg2addnclem  37695  ftc1anc  37725  incsequz  37772  isbnd3  37808  ssbnd  37812  onexomgt  43265  dflim5  43353  corclrcl  43731  imo72b2lem2  44191  imo72b2lem1  44193  imo72b2  44196  amgm2d  44222  nnn0  45405  ren0  45429  ioodvbdlimc1  45962  ioodvbdlimc2  45964  stirlinglem13  46115  fourierdlem103  46238  fourierdlem104  46239  fouriersw  46260  hoicvr  46577  2zlidl  48215  termc2  49403