Theorem ne0ii 4279

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

Syntax hints:   ∈ wcel 2119   ≠ wne 2935  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-dif 3893  df-nul 4269

This theorem is referenced by:  vn0ALT  4281  prnz  4716  tpnz  4718  pwne0  5292  onn0  6383  oawordeulem  8486  noinfep  9579  fin23lem31  10263  isfin1-3  10306  omina  10612  nnunb  12431  rpnnen1lem4  12928  rpnnen1lem5  12929  rexfiuz  15308  caurcvg  15637  caurcvg2  15638  caucvg  15639  infcvgaux1i  15820  divalglem2  16362  pc2dvds  16848  vdwmc2  16948  cnsubglem  21398  cnmsubglem  21412  pzriprnglem4  21466  pmatcollpw3  22774  zfbas  23886  nrginvrcn  24682  lebnumlem3  24955  caun0  25273  cnflduss  25348  cnfldcusp  25349  reust  25373  recusp  25374  nulmbl2  25528  itg2seq  25734  itg2monolem1  25742  c1lip1  25989  aannenlem2  26320  logbmpt  26777  tgcgr4  28624  shintcl  31426  chintcl  31428  nmoprepnf  31963  nmfnrepnf  31976  nmcexi  32122  snct  32811  constrext2chnlem  33941  constrfiss  33942  esum0  34240  esumpcvgval  34269  bnj906  35119  satf0  35607  fmla1  35622  prv0  35665  bj-tagn0  37339  taupi  37690  ismblfin  38035  volsupnfl  38039  itg2addnclem  38045  ftc1anc  38075  incsequz  38122  isbnd3  38158  ssbnd  38162  onexomgt  43693  dflim5  43781  corclrcl  44158  imo72b2lem2  44618  imo72b2lem1  44620  imo72b2  44623  amgm2d  44649  nnn0  45829  ren0  45852  ioodvbdlimc1  46383  ioodvbdlimc2  46385  stirlinglem13  46536  fourierdlem103  46659  fourierdlem104  46660  fouriersw  46681  2zlidl  48738  termc2  50015