Theorem ne0ii 4310

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

Syntax hints:   ∈ wcel 2109   ≠ wne 2926  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-dif 3920  df-nul 4300

This theorem is referenced by:  vn0ALT  4312  prnz  4744  tpnz  4746  pwne0  5315  onn0  6401  oawordeulem  8521  noinfep  9620  fin23lem31  10303  isfin1-3  10346  omina  10651  nnunb  12445  rpnnen1lem4  12946  rpnnen1lem5  12947  rexfiuz  15321  caurcvg  15650  caurcvg2  15651  caucvg  15652  infcvgaux1i  15830  divalglem2  16372  pc2dvds  16857  vdwmc2  16957  cnsubglem  21339  cnmsubglem  21354  pzriprnglem4  21401  pmatcollpw3  22678  zfbas  23790  nrginvrcn  24587  lebnumlem3  24869  caun0  25188  cnflduss  25263  cnfldcusp  25264  reust  25288  recusp  25289  nulmbl2  25444  itg2seq  25650  itg2monolem1  25658  c1lip1  25909  aannenlem2  26244  logbmpt  26705  tgcgr4  28465  shintcl  31266  chintcl  31268  nmoprepnf  31803  nmfnrepnf  31816  nmcexi  31962  snct  32644  constrext2chnlem  33747  constrfiss  33748  esum0  34046  esumpcvgval  34075  bnj906  34927  satf0  35366  fmla1  35381  prv0  35424  bj-tagn0  36974  taupi  37318  ismblfin  37662  volsupnfl  37666  itg2addnclem  37672  ftc1anc  37702  incsequz  37749  isbnd3  37785  ssbnd  37789  onexomgt  43237  dflim5  43325  corclrcl  43703  imo72b2lem2  44163  imo72b2lem1  44165  imo72b2  44168  amgm2d  44194  nnn0  45381  ren0  45405  ioodvbdlimc1  45938  ioodvbdlimc2  45940  stirlinglem13  46091  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  hoicvr  46553  2zlidl  48232  termc2  49511