Theorem ne0ii 4367

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2946  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-dif 3979  df-nul 4353

This theorem is referenced by:  vn0ALT  4369  prnz  4802  tpnz  4804  pwne0  5375  onn0  6460  oawordeulem  8610  noinfep  9729  fin23lem31  10412  isfin1-3  10455  omina  10760  nnunb  12549  rpnnen1lem4  13045  rpnnen1lem5  13046  rexfiuz  15396  caurcvg  15725  caurcvg2  15726  caucvg  15727  infcvgaux1i  15905  divalglem2  16443  pc2dvds  16926  vdwmc2  17026  cnsubglem  21456  cnmsubglem  21471  pzriprnglem4  21518  pmatcollpw3  22811  zfbas  23925  nrginvrcn  24734  lebnumlem3  25014  caun0  25334  cnflduss  25409  cnfldcusp  25410  reust  25434  recusp  25435  nulmbl2  25590  itg2seq  25797  itg2monolem1  25805  c1lip1  26056  aannenlem2  26389  logbmpt  26849  tgcgr4  28557  shintcl  31362  chintcl  31364  nmoprepnf  31899  nmfnrepnf  31912  nmcexi  32058  snct  32727  esum0  34013  esumpcvgval  34042  bnj906  34906  satf0  35340  fmla1  35355  prv0  35398  bj-tagn0  36945  taupi  37289  ismblfin  37621  volsupnfl  37625  itg2addnclem  37631  ftc1anc  37661  incsequz  37708  isbnd3  37744  ssbnd  37748  onexomgt  43202  dflim5  43291  corclrcl  43669  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  amgm2d  44160  nnn0  45293  ren0  45317  ioodvbdlimc1  45854  ioodvbdlimc2  45856  stirlinglem13  46007  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  hoicvr  46469  2zlidl  47963