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 2143   ≠ wne 2958  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 3909  df-nul 4288

This theorem is referenced by:  vn0ALT  4301  prnz  4744  tpnz  4746  pwne0  5329  onn0  6429  oawordeulem  8540  noinfep  9630  fin23lem31  10328  isfin1-3  10371  omina  10677  nnunb  12501  rpnnen1lem4  13005  rpnnen1lem5  13006  rexfiuz  15401  caurcvg  15730  caurcvg2  15731  caucvg  15732  infcvgaux1i  15913  divalglem2  16454  pc2dvds  16940  vdwmc2  17040  cnsubglem  21547  cnmsubglem  21561  pzriprnglem4  21615  pmatcollpw3  22922  zfbas  24034  nrginvrcn  24830  lebnumlem3  25103  caun0  25421  cnflduss  25496  cnfldcusp  25497  reust  25521  recusp  25522  nulmbl2  25676  itg2seq  25882  itg2monolem1  25890  c1lip1  26137  aannenlem2  26473  logbmpt  26934  tgcgr4  28781  shintcl  31663  chintcl  31665  nmoprepnf  32200  nmfnrepnf  32213  nmcexi  32359  snct  33038  constrext2chnlem  34121  constrfiss  34122  esum0  34420  esumpcvgval  34449  bnj906  35299  satf0  35845  fmla1  35860  prv0  35903  bj-tagn0  37596  taupi  37948  ismblfin  38293  volsupnfl  38297  itg2addnclem  38303  ftc1anc  38333  incsequz  38380  isbnd3  38416  ssbnd  38420  onexomgt  43951  dflim5  44039  corclrcl  44416  imo72b2lem2  44876  imo72b2lem1  44878  imo72b2  44881  amgm2d  44907  nnn0  46076  ren0  46099  ioodvbdlimc1  46630  ioodvbdlimc2  46632  stirlinglem13  46783  fourierdlem103  46906  fourierdlem104  46907  fouriersw  46928  2zlidl  48988  termc2  50279