Theorem ne0ii 4289

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

This proof depends on syntax axioms:   ∈ wcel 2144   ≠ wne 2955  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-dif 4047  df-nul 4279

This theorem is used by:  vn0ALT  4292  prnz  4734  tpnz  4736  pwne0  5317  onn0  6429  oawordeulem  8565  noinfep  9664  fin23lem31  10424  isfin1-3  10467  omina  10779  nnunb  12605  rpnnen1lem4  13111  rpnnen1lem5  13112  rexfiuz  15520  caurcvg  15849  caurcvg2  15850  caucvg  15851  infcvgaux1i  16031  divalglem2  16570  pc2dvds  17062  vdwmc2  17162  cnsubglem  21727  cnmsubglem  21741  pzriprnglem4  21795  pmatcollpw3  23107  zfbas  24220  nrginvrcn  25016  lebnumlem3  25289  caun0  25607  cnflduss  25682  cnfldcusp  25683  reust  25707  recusp  25708  nulmbl2  25862  itg2seq  26068  itg2monolem1  26076  c1lip1  26322  aannenlem2  26661  logbmpt  27121  tgcgr4  28999  shintcl  31937  chintcl  31939  nmoprepnf  32474  nmfnrepnf  32487  nmcexi  32633  snct  33352  constrext2chnlem  34428  constrfiss  34429  esum0  34727  esumpcvgval  34756  bnj906  35606  satf0  36223  fmla1  36238  prv0  36281  bj-tagn0  37984  taupi  38337  ismblfin  38672  volsupnfl  38676  itg2addnclem  38682  ftc1anc  38712  incsequz  38775  isbnd3  38811  ssbnd  38815  onexomgt  44336  dflim5  44424  corclrcl  44800  imo72b2lem2  45260  imo72b2lem1  45262  imo72b2  45265  amgm2d  45291  nnn0  46482  ren0  46505  ioodvbdlimc1  47036  ioodvbdlimc2  47038  stirlinglem13  47189  fourierdlem103  47312  fourierdlem104  47313  fouriersw  47334  2zlidl  49430  termc2  50746  veronesematrowd  51149  veroquadmodzerod  51152  veroquadnolindfd  51153