Theorem ne0ii 4344

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

Syntax hints:   ∈ wcel 2108   ≠ wne 2940  ∅c0 4333

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-dif 3954  df-nul 4334

This theorem is referenced by:  vn0ALT  4346  prnz  4777  tpnz  4779  pwne0  5357  onn0  6449  oawordeulem  8592  noinfep  9700  fin23lem31  10383  isfin1-3  10426  omina  10731  nnunb  12522  rpnnen1lem4  13022  rpnnen1lem5  13023  rexfiuz  15386  caurcvg  15713  caurcvg2  15714  caucvg  15715  infcvgaux1i  15893  divalglem2  16432  pc2dvds  16917  vdwmc2  17017  cnsubglem  21433  cnmsubglem  21448  pzriprnglem4  21495  pmatcollpw3  22790  zfbas  23904  nrginvrcn  24713  lebnumlem3  24995  caun0  25315  cnflduss  25390  cnfldcusp  25391  reust  25415  recusp  25416  nulmbl2  25571  itg2seq  25777  itg2monolem1  25785  c1lip1  26036  aannenlem2  26371  logbmpt  26831  tgcgr4  28539  shintcl  31349  chintcl  31351  nmoprepnf  31886  nmfnrepnf  31899  nmcexi  32045  snct  32725  esum0  34050  esumpcvgval  34079  bnj906  34944  satf0  35377  fmla1  35392  prv0  35435  bj-tagn0  36980  taupi  37324  ismblfin  37668  volsupnfl  37672  itg2addnclem  37678  ftc1anc  37708  incsequz  37755  isbnd3  37791  ssbnd  37795  onexomgt  43253  dflim5  43342  corclrcl  43720  imo72b2lem2  44180  imo72b2lem1  44182  imo72b2  44185  amgm2d  44211  nnn0  45389  ren0  45413  ioodvbdlimc1  45948  ioodvbdlimc2  45950  stirlinglem13  46101  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  hoicvr  46563  2zlidl  48156  termc2  49148