Theorem ne0i 4268

Description: If a class has elements, then it is nonempty. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
ne0i	⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 4267	. 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
2	1	neqned 2950	1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2943  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-dif 3889  df-nul 4257

This theorem is referenced by:  ne0d  4269  ne0ii  4271  inelcm  4398  rzalALT  4440  rexn0OLD  4445  2reu4  4457  tpnzd  4716  issn  4763  brne0  5123  ord0eln0  6313  elfvmptrab1  6894  elovmpt3imp  7516  onnmin  7638  f1oweALT  7804  brovpreldm  7916  bropopvvv  7917  frxp  7954  mpoxopxnop0  8018  brovex  8025  ord1eln01  8313  ord2eln012  8314  oe1m  8363  oa00  8377  oarec  8380  omord  8386  omeulem1  8400  oewordri  8410  oeordsuc  8412  oelim2  8413  nnmord  8450  map0g  8659  ixpn0  8705  unblem1  9053  wofib  9291  canthwdom  9325  inf1  9367  oemapvali  9429  cantnf  9438  epfrs  9498  acnrcl  9808  iunfictbso  9880  dfac5lem2  9890  kmlem6  9921  fin23lem40  10117  isf34lem7  10145  isf34lem6  10146  fin1a2lem7  10172  fin1a2lem13  10178  alephval2  10338  tskpr  10536  inar1  10541  tskuni  10549  tskxp  10553  tskmap  10554  grur1  10586  axgroth3  10597  inaprc  10602  addclpi  10658  indpi  10673  nqerf  10696  genpn0  10769  infrelb  11970  infssuzle  12681  eliooxr  13147  iccssioo2  13162  iccsupr  13184  elfzoel1  13395  elfzoel2  13396  fzon0  13415  fseqsupubi  13708  hashnn0n0nn  14116  pfxn0  14409  r19.2uz  15073  climuni  15271  ruclem11  15959  bezoutlem2  16258  lcmgcdlem  16321  prmreclem6  16632  vdwlem8  16699  ramtcl  16721  catcone0  17406  fpwipodrs  18268  gsumval2  18380  mgm2nsgrplem1  18567  sgrp2nmndlem1  18572  issubg3  18783  brgici  18896  odlem2  19157  gexlem2  19197  sylow3lem3  19244  abln0  19478  cyggexb  19510  gsumval3  19518  ablfacrp2  19680  ablfac1c  19684  pgpfaclem2  19695  ringn0  19852  subrgugrp  20053  brlmici  20341  01eq0ring  20553  mpllsslem  21216  ltbwe  21255  mpfrcl  21305  ply1plusgfvi  21423  ply1frcl  21494  cramerimplem2  21843  cramerimplem3  21844  cramerimp  21845  clsval2  22211  lmmo  22541  1stcfb  22606  2ndcsep  22620  ptclsg  22776  txindis  22795  hmphi  22938  trfbas2  23004  flimclslem  23145  ustfilxp  23374  prdsmet  23533  prdsbl  23657  tgioo  23969  caun0  24455  ovolctb  24664  mbflimsup  24840  itg1climres  24889  itg2i1fseq2  24931  dvferm1lem  25158  dvferm2lem  25160  dvferm  25162  c1liplem1  25170  dvivthlem1  25182  aalioulem2  25503  birthdaylem1  26111  tgldimor  26873  axlowdimlem13  27332  uvtx01vtx  27774  wlkreslem  28046  wspniunwspnon  28296  usgr2wspthons3  28337  rusgrnumwwlks  28347  rusgrnumwwlk  28348  frgr2wwlkn0  28700  numclwwlk1  28733  numclwlk1lem1  28741  numclwwlk3  28757  numclwwlk5  28760  ubthlem1  29240  eldmne0  30971  drgextlsp  31689  dimval  31694  dimvalfi  31695  zarcls1  31827  rge0scvg  31907  qqhucn  31950  voliune  32205  eulerpartlemt  32346  erdszelem2  33162  dfso3  33672  sltval2  33867  fnemeet1  34563  fnejoin1  34565  tailfb  34574  curfv  35765  ptrecube  35785  poimirlem23  35808  poimirlem31  35816  poimirlem32  35817  mblfinlem2  35823  ismblfin  35826  ovoliunnfl  35827  voliunnfl  35829  itg2addnc  35839  totbndbnd  35955  prdsbnd  35959  heibor1lem  35975  prtlem100  36881  prter3  36904  ishlat3N  37376  hlsupr2  37409  elpaddri  37824  diaintclN  39080  dibintclN  39189  dihintcl  39366  rencldnfi  40651  neik0imk0p  41627  clsk3nimkb  41631  amgm3d  41791  amgm4d  41792  prmunb2  41910  rzalf  42541  pwfin0  42591  ssuzfz  42869  fsumiunss  43097  limsupvaluz2  43260  supcnvlimsup  43262  jumpncnp  43420  ioodvbdlimc1lem2  43454  ioodvbdlimc2lem  43456  stoweidlem11  43533  stoweidlem31  43553  stoweidlem34  43556  stoweidlem59  43581  fourierdlem31  43660  fourierdlem42  43671  fourierdlem48  43676  fourierdlem49  43677  fourierdlem64  43692  fourierdlem73  43701  fourierdlem79  43707  qndenserrnbllem  43816  qndenserrn  43821  sge0rnn0  43887  hoidmvlelem1  44114  hoidmvlelem2  44115  hoidmvlelem4  44117  ovnlecvr2  44129  hspmbllem2  44146  vonioo  44201  vonicc  44204  smflimsuplem1  44331  smflimsuplem2  44332  cznrng  45491  lmodn0  45814  elfvne0  46154  aacllem  46483  amgmw2d  46486