Theorem ne0ii 4296

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

Syntax hints:   ∈ wcel 2113   ≠ wne 2932  ∅c0 4285

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3904  df-nul 4286

This theorem is referenced by:  vn0ALT  4298  prnz  4734  tpnz  4736  pwne0  5302  onn0  6383  oawordeulem  8481  noinfep  9569  fin23lem31  10253  isfin1-3  10296  omina  10602  nnunb  12397  rpnnen1lem4  12893  rpnnen1lem5  12894  rexfiuz  15271  caurcvg  15600  caurcvg2  15601  caucvg  15602  infcvgaux1i  15780  divalglem2  16322  pc2dvds  16807  vdwmc2  16907  cnsubglem  21370  cnmsubglem  21385  pzriprnglem4  21439  pmatcollpw3  22728  zfbas  23840  nrginvrcn  24636  lebnumlem3  24918  caun0  25237  cnflduss  25312  cnfldcusp  25313  reust  25337  recusp  25338  nulmbl2  25493  itg2seq  25699  itg2monolem1  25707  c1lip1  25958  aannenlem2  26293  logbmpt  26754  tgcgr4  28603  shintcl  31405  chintcl  31407  nmoprepnf  31942  nmfnrepnf  31955  nmcexi  32101  snct  32791  constrext2chnlem  33907  constrfiss  33908  esum0  34206  esumpcvgval  34235  bnj906  35086  satf0  35566  fmla1  35581  prv0  35624  bj-tagn0  37180  taupi  37528  ismblfin  37862  volsupnfl  37866  itg2addnclem  37872  ftc1anc  37902  incsequz  37949  isbnd3  37985  ssbnd  37989  onexomgt  43483  dflim5  43571  corclrcl  43948  imo72b2lem2  44408  imo72b2lem1  44410  imo72b2  44413  amgm2d  44439  nnn0  45622  ren0  45646  ioodvbdlimc1  46177  ioodvbdlimc2  46179  stirlinglem13  46330  fourierdlem103  46453  fourierdlem104  46454  fouriersw  46475  hoicvr  46792  2zlidl  48486  termc2  49763