Theorem ne0ii 4290

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

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2955  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-dif 3902  df-nul 4280

This theorem is used by:  vn0ALT  4293  prnz  4738  tpnz  4740  pwne0  5321  onn0  6424  oawordeulem  8542  noinfep  9640  fin23lem31  10346  isfin1-3  10389  omina  10701  nnunb  12525  rpnnen1lem4  13031  rpnnen1lem5  13032  rexfiuz  15436  caurcvg  15765  caurcvg2  15766  caucvg  15767  infcvgaux1i  15947  divalglem2  16486  pc2dvds  16972  vdwmc2  17072  cnsubglem  21630  cnmsubglem  21644  pzriprnglem4  21698  pmatcollpw3  23010  zfbas  24123  nrginvrcn  24919  lebnumlem3  25192  caun0  25510  cnflduss  25585  cnfldcusp  25586  reust  25610  recusp  25611  nulmbl2  25765  itg2seq  25971  itg2monolem1  25979  c1lip1  26225  aannenlem2  26566  logbmpt  27026  tgcgr4  28874  shintcl  31812  chintcl  31814  nmoprepnf  32349  nmfnrepnf  32362  nmcexi  32508  snct  33185  constrext2chnlem  34261  constrfiss  34262  esum0  34560  esumpcvgval  34589  bnj906  35440  satf0  35952  fmla1  35967  prv0  36010  bj-tagn0  37724  taupi  38076  ismblfin  38411  volsupnfl  38415  itg2addnclem  38421  ftc1anc  38451  incsequz  38499  isbnd3  38535  ssbnd  38539  onexomgt  44083  dflim5  44171  corclrcl  44548  imo72b2lem2  45008  imo72b2lem1  45010  imo72b2  45013  amgm2d  45039  nnn0  46208  ren0  46231  ioodvbdlimc1  46762  ioodvbdlimc2  46764  stirlinglem13  46915  fourierdlem103  47038  fourierdlem104  47039  fouriersw  47060  2zlidl  49156  termc2  50445  veronesematrowd  50815  veroquadmodzerod  50818  veroquadnolindfd  50819