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 2141   ≠ wne 2956  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3907  df-nul 4286

This theorem is referenced by:  vn0ALT  4298  prnz  4735  tpnz  4737  pwne0  5312  onn0  6408  oawordeulem  8518  noinfep  9612  fin23lem31  10297  isfin1-3  10340  omina  10646  nnunb  12474  rpnnen1lem4  12978  rpnnen1lem5  12979  rexfiuz  15358  caurcvg  15687  caurcvg2  15688  caucvg  15689  infcvgaux1i  15870  divalglem2  16412  pc2dvds  16898  vdwmc2  16998  cnsubglem  21448  cnmsubglem  21462  pzriprnglem4  21516  pmatcollpw3  22824  zfbas  23936  nrginvrcn  24732  lebnumlem3  25005  caun0  25323  cnflduss  25398  cnfldcusp  25399  reust  25423  recusp  25424  nulmbl2  25578  itg2seq  25784  itg2monolem1  25792  c1lip1  26039  aannenlem2  26370  logbmpt  26830  tgcgr4  28677  shintcl  31479  chintcl  31481  nmoprepnf  32016  nmfnrepnf  32029  nmcexi  32175  snct  32864  constrext2chnlem  34008  constrfiss  34009  esum0  34307  esumpcvgval  34336  bnj906  35189  satf0  35686  fmla1  35701  prv0  35744  bj-tagn0  37428  taupi  37779  ismblfin  38124  volsupnfl  38128  itg2addnclem  38134  ftc1anc  38164  incsequz  38211  isbnd3  38247  ssbnd  38251  onexomgt  43782  dflim5  43870  corclrcl  44247  imo72b2lem2  44707  imo72b2lem1  44709  imo72b2  44712  amgm2d  44738  nnn0  45917  ren0  45940  ioodvbdlimc1  46471  ioodvbdlimc2  46473  stirlinglem13  46624  fourierdlem103  46747  fourierdlem104  46748  fouriersw  46769  2zlidl  48826  termc2  50103