Theorem ne0ii 4293

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

This proof depends on syntax axioms:   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-dif 4050  df-nul 4282

This theorem is used by:  vn0ALT  4296  prnz  4738  tpnz  4740  pwne0  5323  onn0  6450  oawordeulem  8593  noinfep  9691  fin23lem31  10451  isfin1-3  10494  omina  10806  nnunb  12632  rpnnen1lem4  13138  rpnnen1lem5  13139  rexfiuz  15547  caurcvg  15876  caurcvg2  15877  caucvg  15878  infcvgaux1i  16058  divalglem2  16597  pc2dvds  17089  vdwmc2  17189  cnsubglem  21755  cnmsubglem  21769  pzriprnglem4  21823  pmatcollpw3  23135  zfbas  24248  nrginvrcn  25044  lebnumlem3  25317  caun0  25635  cnflduss  25710  cnfldcusp  25711  reust  25735  recusp  25736  nulmbl2  25890  itg2seq  26096  itg2monolem1  26104  c1lip1  26350  aannenlem2  26689  logbmpt  27149  tgcgr4  29027  shintcl  31965  chintcl  31967  nmoprepnf  32502  nmfnrepnf  32515  nmcexi  32661  snct  33379  constrext2chnlem  34465  constrfiss  34466  esum0  34764  esumpcvgval  34793  bnj906  35643  j0le  36032  k3n0j0lt  36033  satf0  36317  fmla1  36332  prv0  36375  bj-tagn0  38083  taupi  38449  ismblfin  38784  volsupnfl  38788  itg2addnclem  38794  ftc1anc  38824  incsequz  38885  isbnd3  38921  ssbnd  38925  onexomgt  44446  dflim5  44534  corclrcl  44910  imo72b2lem2  45370  imo72b2lem1  45372  imo72b2  45375  amgm2d  45401  nnn0  46604  ren0  46627  ioodvbdlimc1  47158  ioodvbdlimc2  47160  stirlinglem13  47311  fourierdlem103  47434  fourierdlem104  47435  fouriersw  47456  2zlidl  49552  termc2  50868  veronesematrowd  51293  veroquadmodzerod  51296  veroquadnolindfd  51297