Theorem ne0ii 4285

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

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

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 3893  df-nul 4275

This theorem is referenced by:  vn0ALT  4287  prnz  4722  tpnz  4724  pwne0  5294  onn0  6383  oawordeulem  8482  noinfep  9572  fin23lem31  10256  isfin1-3  10299  omina  10605  nnunb  12424  rpnnen1lem4  12921  rpnnen1lem5  12922  rexfiuz  15301  caurcvg  15630  caurcvg2  15631  caucvg  15632  infcvgaux1i  15813  divalglem2  16355  pc2dvds  16841  vdwmc2  16941  cnsubglem  21405  cnmsubglem  21420  pzriprnglem4  21474  pmatcollpw3  22759  zfbas  23871  nrginvrcn  24667  lebnumlem3  24940  caun0  25258  cnflduss  25333  cnfldcusp  25334  reust  25358  recusp  25359  nulmbl2  25513  itg2seq  25719  itg2monolem1  25727  c1lip1  25974  aannenlem2  26306  logbmpt  26765  tgcgr4  28613  shintcl  31416  chintcl  31418  nmoprepnf  31953  nmfnrepnf  31966  nmcexi  32112  snct  32800  constrext2chnlem  33910  constrfiss  33911  esum0  34209  esumpcvgval  34238  bnj906  35088  satf0  35570  fmla1  35585  prv0  35628  bj-tagn0  37302  taupi  37653  ismblfin  37996  volsupnfl  38000  itg2addnclem  38006  ftc1anc  38036  incsequz  38083  isbnd3  38119  ssbnd  38123  onexomgt  43687  dflim5  43775  corclrcl  44152  imo72b2lem2  44612  imo72b2lem1  44614  imo72b2  44617  amgm2d  44643  nnn0  45825  ren0  45848  ioodvbdlimc1  46379  ioodvbdlimc2  46381  stirlinglem13  46532  fourierdlem103  46655  fourierdlem104  46656  fouriersw  46677  2zlidl  48728  termc2  50005