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  37524  ismblfin  37858  volsupnfl  37862  itg2addnclem  37868  ftc1anc  37898  incsequz  37945  isbnd3  37981  ssbnd  37985  onexomgt  43479  dflim5  43567  corclrcl  43944  imo72b2lem2  44404  imo72b2lem1  44406  imo72b2  44409  amgm2d  44435  nnn0  45618  ren0  45642  ioodvbdlimc1  46173  ioodvbdlimc2  46175  stirlinglem13  46326  fourierdlem103  46449  fourierdlem104  46450  fouriersw  46471  hoicvr  46788  2zlidl  48482  termc2  49759