Theorem ne0ii 4300

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

This proof depends on syntax axioms:   ∈ wcel 2146   ≠ wne 2961  ∅c0 4289

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-dif 3911  df-nul 4290

This theorem is used by:  vn0ALT  4303  prnz  4748  tpnz  4750  pwne0  5332  onn0  6434  oawordeulem  8548  noinfep  9639  fin23lem31  10345  isfin1-3  10388  omina  10694  nnunb  12518  rpnnen1lem4  13022  rpnnen1lem5  13023  rexfiuz  15425  caurcvg  15754  caurcvg2  15755  caucvg  15756  infcvgaux1i  15937  divalglem2  16478  pc2dvds  16964  vdwmc2  17064  cnsubglem  21603  cnmsubglem  21617  pzriprnglem4  21671  pmatcollpw3  22978  zfbas  24090  nrginvrcn  24886  lebnumlem3  25159  caun0  25477  cnflduss  25552  cnfldcusp  25553  reust  25577  recusp  25578  nulmbl2  25732  itg2seq  25938  itg2monolem1  25946  c1lip1  26193  aannenlem2  26529  logbmpt  26990  tgcgr4  28837  shintcl  31719  chintcl  31721  nmoprepnf  32256  nmfnrepnf  32269  nmcexi  32415  snct  33094  constrext2chnlem  34171  constrfiss  34172  esum0  34470  esumpcvgval  34499  bnj906  35350  satf0  35885  fmla1  35900  prv0  35943  bj-tagn0  37656  taupi  38008  ismblfin  38353  volsupnfl  38357  itg2addnclem  38363  ftc1anc  38393  incsequz  38440  isbnd3  38476  ssbnd  38480  onexomgt  44009  dflim5  44097  corclrcl  44474  imo72b2lem2  44934  imo72b2lem1  44936  imo72b2  44939  amgm2d  44965  nnn0  46134  ren0  46157  ioodvbdlimc1  46688  ioodvbdlimc2  46690  stirlinglem13  46841  fourierdlem103  46964  fourierdlem104  46965  fouriersw  46986  2zlidl  49046  termc2  50337