Theorem ne0ii 4294

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

Syntax hints:   ∈ wcel 2111   ≠ wne 2928  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-dif 3905  df-nul 4284

This theorem is referenced by:  vn0ALT  4296  prnz  4730  tpnz  4732  pwne0  5295  onn0  6372  oawordeulem  8469  noinfep  9550  fin23lem31  10234  isfin1-3  10277  omina  10582  nnunb  12377  rpnnen1lem4  12878  rpnnen1lem5  12879  rexfiuz  15255  caurcvg  15584  caurcvg2  15585  caucvg  15586  infcvgaux1i  15764  divalglem2  16306  pc2dvds  16791  vdwmc2  16891  cnsubglem  21353  cnmsubglem  21368  pzriprnglem4  21422  pmatcollpw3  22700  zfbas  23812  nrginvrcn  24608  lebnumlem3  24890  caun0  25209  cnflduss  25284  cnfldcusp  25285  reust  25309  recusp  25310  nulmbl2  25465  itg2seq  25671  itg2monolem1  25679  c1lip1  25930  aannenlem2  26265  logbmpt  26726  tgcgr4  28510  shintcl  31308  chintcl  31310  nmoprepnf  31845  nmfnrepnf  31858  nmcexi  32004  snct  32693  constrext2chnlem  33761  constrfiss  33762  esum0  34060  esumpcvgval  34089  bnj906  34940  satf0  35414  fmla1  35429  prv0  35472  bj-tagn0  37019  taupi  37363  ismblfin  37707  volsupnfl  37711  itg2addnclem  37717  ftc1anc  37747  incsequz  37794  isbnd3  37830  ssbnd  37834  onexomgt  43280  dflim5  43368  corclrcl  43746  imo72b2lem2  44206  imo72b2lem1  44208  imo72b2  44211  amgm2d  44237  nnn0  45422  ren0  45446  ioodvbdlimc1  45977  ioodvbdlimc2  45979  stirlinglem13  46130  fourierdlem103  46253  fourierdlem104  46254  fouriersw  46275  hoicvr  46592  2zlidl  48277  termc2  49556