Theorem ne0ii 4226

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

Syntax hints:   ∈ wcel 2114   ≠ wne 2934  ∅c0 4211

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-dif 3846  df-nul 4212

This theorem is referenced by:  vn0ALT  4228  prnz  4668  tpnz  4670  pwne0  5223  onn0  6236  oawordeulem  8213  noinfep  9198  fin23lem31  9845  isfin1-3  9888  omina  10193  nnunb  11974  rpnnen1lem4  12464  rpnnen1lem5  12465  rexfiuz  14799  caurcvg  15128  caurcvg2  15129  caucvg  15130  infcvgaux1i  15307  divalglem2  15842  pc2dvds  16317  vdwmc2  16417  cnsubglem  20268  cnmsubglem  20282  pmatcollpw3  21537  zfbas  22649  nrginvrcn  23447  lebnumlem3  23717  caun0  24035  cnflduss  24110  cnfldcusp  24111  reust  24135  recusp  24136  nulmbl2  24290  itg2seq  24497  itg2monolem1  24505  c1lip1  24751  aannenlem2  25079  logbmpt  25528  tgcgr4  26479  shintcl  29267  chintcl  29269  nmoprepnf  29804  nmfnrepnf  29817  nmcexi  29963  snct  30625  esum0  31589  esumpcvgval  31618  bnj906  32483  satf0  32907  fmla1  32922  prv0  32965  bj-tagn0  34814  taupi  35136  ismblfin  35463  volsupnfl  35467  itg2addnclem  35473  ftc1anc  35503  incsequz  35551  isbnd3  35587  ssbnd  35591  corclrcl  40883  imo72b2lem0  41344  imo72b2lem2  41346  imo72b2lem1  41348  imo72b2  41352  amgm2d  41378  nnn0  42477  ren0  42502  ioodvbdlimc1  43038  ioodvbdlimc2  43040  stirlinglem13  43191  fourierdlem103  43314  fourierdlem104  43315  fouriersw  43336  hoicvr  43650  2zlidl  45055