Theorem ne0ii 4293

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

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2957  ∅c0 4282

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-dif 3905  df-nul 4283

This theorem is used by:  vn0ALT  4296  prnz  4741  tpnz  4743  pwne0  5325  onn0  6428  oawordeulem  8545  noinfep  9643  fin23lem31  10349  isfin1-3  10392  omina  10704  nnunb  12528  rpnnen1lem4  13034  rpnnen1lem5  13035  rexfiuz  15439  caurcvg  15768  caurcvg2  15769  caucvg  15770  infcvgaux1i  15950  divalglem2  16491  pc2dvds  16977  vdwmc2  17077  cnsubglem  21635  cnmsubglem  21649  pzriprnglem4  21703  pmatcollpw3  23015  zfbas  24128  nrginvrcn  24924  lebnumlem3  25197  caun0  25515  cnflduss  25590  cnfldcusp  25591  reust  25615  recusp  25616  nulmbl2  25770  itg2seq  25976  itg2monolem1  25984  c1lip1  26231  aannenlem2  26572  logbmpt  27033  tgcgr4  28881  shintcl  31819  chintcl  31821  nmoprepnf  32356  nmfnrepnf  32369  nmcexi  32515  snct  33192  constrext2chnlem  34268  constrfiss  34269  esum0  34567  esumpcvgval  34596  bnj906  35447  satf0  35959  fmla1  35974  prv0  36017  bj-tagn0  37731  taupi  38083  ismblfin  38418  volsupnfl  38422  itg2addnclem  38428  ftc1anc  38458  incsequz  38506  isbnd3  38542  ssbnd  38546  onexomgt  44090  dflim5  44178  corclrcl  44555  imo72b2lem2  45015  imo72b2lem1  45017  imo72b2  45020  amgm2d  45046  nnn0  46215  ren0  46238  ioodvbdlimc1  46769  ioodvbdlimc2  46771  stirlinglem13  46922  fourierdlem103  47045  fourierdlem104  47046  fouriersw  47067  2zlidl  49163  termc2  50452  veronesematrowd  50822  veroquadmodzerod  50825  veroquadnolindfd  50826