Theorem ne0i 4269

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 4268	. 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅)
2	1	neqned 2951	1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2944  ∅c0 4257

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-dif 3891  df-nul 4258

This theorem is referenced by:  ne0d  4270  ne0ii  4272  inelcm  4399  rzalALT  4441  rexn0OLD  4446  2reu4  4458  tpnzd  4717  issn  4764  brne0  5125  ord0eln0  6324  elfvmptrab1  6911  elovmpt3imp  7535  onnmin  7657  f1oweALT  7824  brovpreldm  7938  bropopvvv  7939  frxp  7976  mpoxopxnop0  8040  brovex  8047  ord1eln01  8335  ord2eln012  8336  oe1m  8385  oa00  8399  oarec  8402  omord  8408  omeulem1  8422  oewordri  8432  oeordsuc  8434  oelim2  8435  nnmord  8472  map0g  8681  ixpn0  8727  unblem1  9075  wofib  9313  canthwdom  9347  inf1  9389  oemapvali  9451  cantnf  9460  epfrs  9498  acnrcl  9807  iunfictbso  9879  dfac5lem2  9889  kmlem6  9920  fin23lem40  10116  isf34lem7  10144  isf34lem6  10145  fin1a2lem7  10171  fin1a2lem13  10177  alephval2  10337  tskpr  10535  inar1  10540  tskuni  10548  tskxp  10552  tskmap  10553  grur1  10585  axgroth3  10596  inaprc  10601  addclpi  10657  indpi  10672  nqerf  10695  genpn0  10768  infrelb  11969  infssuzle  12680  eliooxr  13146  iccssioo2  13161  iccsupr  13183  elfzoel1  13394  elfzoel2  13395  fzon0  13414  fseqsupubi  13707  hashnn0n0nn  14115  pfxn0  14408  r19.2uz  15072  climuni  15270  ruclem11  15958  bezoutlem2  16257  lcmgcdlem  16320  prmreclem6  16631  vdwlem8  16698  ramtcl  16720  catcone0  17405  fpwipodrs  18267  gsumval2  18379  mgm2nsgrplem1  18566  sgrp2nmndlem1  18571  issubg3  18782  brgici  18895  odlem2  19156  gexlem2  19196  sylow3lem3  19243  abln0  19477  cyggexb  19509  gsumval3  19517  ablfacrp2  19679  ablfac1c  19683  pgpfaclem2  19694  ringn0  19851  subrgugrp  20052  brlmici  20340  01eq0ring  20552  mpllsslem  21215  ltbwe  21254  mpfrcl  21304  ply1plusgfvi  21422  ply1frcl  21493  cramerimplem2  21842  cramerimplem3  21843  cramerimp  21844  clsval2  22210  lmmo  22540  1stcfb  22605  2ndcsep  22619  ptclsg  22775  txindis  22794  hmphi  22937  trfbas2  23003  flimclslem  23144  ustfilxp  23373  prdsmet  23532  prdsbl  23656  tgioo  23968  caun0  24454  ovolctb  24663  mbflimsup  24839  itg1climres  24888  itg2i1fseq2  24930  dvferm1lem  25157  dvferm2lem  25159  dvferm  25161  c1liplem1  25169  dvivthlem1  25181  aalioulem2  25502  birthdaylem1  26110  tgldimor  26872  axlowdimlem13  27331  uvtx01vtx  27773  wlkreslem  28046  wspniunwspnon  28297  usgr2wspthons3  28338  rusgrnumwwlks  28348  rusgrnumwwlk  28349  frgr2wwlkn0  28701  numclwwlk1  28734  numclwlk1lem1  28742  numclwwlk3  28758  numclwwlk5  28761  ubthlem1  29241  eldmne0  30972  drgextlsp  31690  dimval  31695  dimvalfi  31696  zarcls1  31828  rge0scvg  31908  qqhucn  31951  voliune  32206  eulerpartlemt  32347  erdszelem2  33163  dfso3  33673  sltval2  33868  fnemeet1  34564  fnejoin1  34566  tailfb  34575  curfv  35766  ptrecube  35786  poimirlem23  35809  poimirlem31  35817  poimirlem32  35818  mblfinlem2  35824  ismblfin  35827  ovoliunnfl  35828  voliunnfl  35830  itg2addnc  35840  totbndbnd  35956  prdsbnd  35960  heibor1lem  35976  prtlem100  36880  prter3  36903  ishlat3N  37375  hlsupr2  37408  elpaddri  37823  diaintclN  39079  dibintclN  39188  dihintcl  39365  rencldnfi  40650  neik0imk0p  41653  clsk3nimkb  41657  amgm3d  41817  amgm4d  41818  prmunb2  41936  rzalf  42567  pwfin0  42617  ssuzfz  42895  fsumiunss  43123  limsupvaluz2  43286  supcnvlimsup  43288  jumpncnp  43446  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweidlem11  43559  stoweidlem31  43579  stoweidlem34  43582  stoweidlem59  43607  fourierdlem31  43686  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem64  43718  fourierdlem73  43727  fourierdlem79  43733  qndenserrnbllem  43842  qndenserrn  43847  sge0rnn0  43913  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem4  44143  ovnlecvr2  44155  hspmbllem2  44172  vonioo  44227  vonicc  44230  smflimsuplem1  44364  smflimsuplem2  44365  cznrng  45524  lmodn0  45847  elfvne0  46187  aacllem  46516  amgmw2d  46519