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 ⊢ 𝐵 ≠ ∅

Syntax hints:   ∈ wcel 2113   ≠ wne 2929  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-dif 3901  df-nul 4283

This theorem is referenced by:  vn0ALT  4295  prnz  4731  tpnz  4733  pwne0  5299  onn0  6379  oawordeulem  8477  noinfep  9559  fin23lem31  10243  isfin1-3  10286  omina  10591  nnunb  12386  rpnnen1lem4  12882  rpnnen1lem5  12883  rexfiuz  15259  caurcvg  15588  caurcvg2  15589  caucvg  15590  infcvgaux1i  15768  divalglem2  16310  pc2dvds  16795  vdwmc2  16895  cnsubglem  21356  cnmsubglem  21371  pzriprnglem4  21425  pmatcollpw3  22702  zfbas  23814  nrginvrcn  24610  lebnumlem3  24892  caun0  25211  cnflduss  25286  cnfldcusp  25287  reust  25311  recusp  25312  nulmbl2  25467  itg2seq  25673  itg2monolem1  25681  c1lip1  25932  aannenlem2  26267  logbmpt  26728  tgcgr4  28512  shintcl  31314  chintcl  31316  nmoprepnf  31851  nmfnrepnf  31864  nmcexi  32010  snct  32701  constrext2chnlem  33786  constrfiss  33787  esum0  34085  esumpcvgval  34114  bnj906  34965  satf0  35439  fmla1  35454  prv0  35497  bj-tagn0  37046  taupi  37390  ismblfin  37724  volsupnfl  37728  itg2addnclem  37734  ftc1anc  37764  incsequz  37811  isbnd3  37847  ssbnd  37851  onexomgt  43361  dflim5  43449  corclrcl  43827  imo72b2lem2  44287  imo72b2lem1  44289  imo72b2  44292  amgm2d  44318  nnn0  45503  ren0  45527  ioodvbdlimc1  46058  ioodvbdlimc2  46060  stirlinglem13  46211  fourierdlem103  46334  fourierdlem104  46335  fouriersw  46356  hoicvr  46673  2zlidl  48367  termc2  49646