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 2941	1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2119   ≠ wne 2934  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-dif 3886  df-nul 4262

This theorem is referenced by:  ne0d  4270  ne0ii  4272  inelcm  4393  rzalALT  4423  2reu4  4452  tpnzd  4712  issn  4763  brne0  5122  ord0eln0  6366  elfvunirn  6857  elfvmptrab1  6964  elovmpt3imp  7613  onnmin  7741  f1oweALT  7914  brovpreldm  8028  bropopvvv  8029  frxp  8066  mpoxopxnop0  8155  brovex  8162  ord1eln01  8421  ord2eln012  8422  oe1m  8470  oa00  8484  oarec  8487  omord  8493  omeulem1  8507  oewordri  8518  oeordsuc  8520  oelim2  8521  nnmord  8558  map0g  8822  ixpn0  8868  unblem1  9192  wofib  9450  canthwdom  9484  inf1  9534  oemapvali  9596  cantnf  9605  epfrs  9643  acnrcl  9955  iunfictbso  10027  dfac5lem2  10037  kmlem6  10069  fin23lem40  10264  isf34lem7  10292  isf34lem6  10293  fin1a2lem7  10319  fin1a2lem13  10325  alephval2  10486  tskpr  10684  inar1  10689  tskuni  10697  tskxp  10701  tskmap  10702  grur1  10734  axgroth3  10745  inaprc  10750  addclpi  10806  indpi  10821  nqerf  10844  genpn0  10917  infrelb  12132  infssuzle  12872  eliooxr  13348  iccssioo2  13363  iccsupr  13386  elfzoel1  13602  elfzoel2  13603  fzon0  13623  fseqsupubi  13931  hashnn0n0nn  14344  pfxn0  14640  r19.2uz  15305  climuni  15505  ruclem11  16198  bezoutlem2  16500  lcmgcdlem  16566  prmreclem6  16883  vdwlem8  16950  ramtcl  16972  catcone0  17644  fpwipodrs  18497  gsumval2  18645  mgm2nsgrplem1  18880  sgrp2nmndlem1  18885  issubg3  19111  brgici  19237  odlem2  19505  gexlem2  19548  sylow3lem3  19595  abln0  19833  cyggexb  19865  gsumval3  19873  ablfacrp2  20035  ablfac1c  20039  pgpfaclem2  20050  ringn0  20283  brrici  20476  01eq0ringOLD  20503  subrgugrp  20563  brlmici  21059  mpllsslem  21974  ltbwe  22020  mpfrcl  22061  ply1plusgfvi  22226  ply1frcl  22304  cramerimplem2  22667  cramerimplem3  22668  cramerimp  22669  clsval2  23033  lmmo  23363  1stcfb  23428  2ndcsep  23442  ptclsg  23598  txindis  23617  hmphi  23760  trfbas2  23826  flimclslem  23967  ustfilxp  24196  prdsmet  24353  prdsbl  24474  tgioo  24779  caun0  25266  ovolctb  25475  mbflimsup  25651  itg1climres  25699  itg2i1fseq2  25741  dvferm1lem  25969  dvferm2lem  25971  dvferm  25973  c1liplem1  25981  dvivthlem1  25993  aalioulem2  26317  birthdaylem1  26933  ltsval2  27638  nobdaymin  27763  tgldimor  28588  axlowdimlem13  29041  uvtx01vtx  29484  wlkreslem  29754  wspniunwspnon  30009  usgr2wspthons3  30053  rusgrnumwwlks  30063  rusgrnumwwlk  30064  frgr2wwlkn0  30416  numclwwlk1  30449  numclwlk1lem1  30457  numclwwlk3  30473  numclwwlk5  30476  ubthlem1  30959  n0nsnel  32603  eldmne0  32719  drgextlsp  33778  dimval  33785  dimvalfi  33786  zarcls1  34053  rge0scvg  34133  qqhucn  34176  voliune  34413  eulerpartlemt  34555  erdszelem2  35420  dfso3  35948  fnemeet1  36594  fnejoin1  36596  tailfb  36605  ttc0elw  36755  ttc0el  36763  curfv  37967  ptrecube  37987  poimirlem23  38010  poimirlem31  38018  poimirlem32  38019  mblfinlem2  38025  ismblfin  38028  ovoliunnfl  38029  voliunnfl  38031  itg2addnc  38041  totbndbnd  38156  prdsbnd  38160  heibor1lem  38176  eldisjdmqsim  39184  prtlem100  39351  prter3  39374  ishlat3N  39846  hlsupr2  39879  elpaddri  40294  diaintclN  41550  dibintclN  41659  dihintcl  41836  unitscyglem4  42683  rencldnfi  43266  omlimcl2  43687  oaun3lem1  43819  neik0imk0p  44480  clsk3nimkb  44484  amgm3d  44643  amgm4d  44644  prmunb2  44755  rzalf  45465  pwfin0  45510  ssuzfz  45794  fsumiunss  46020  limsupvaluz2  46181  supcnvlimsup  46183  jumpncnp  46341  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem11  46454  stoweidlem31  46474  stoweidlem34  46477  stoweidlem59  46502  fourierdlem31  46581  fourierdlem42  46592  fourierdlem48  46597  fourierdlem49  46598  fourierdlem64  46613  fourierdlem73  46622  fourierdlem79  46628  qndenserrnbllem  46737  qndenserrn  46742  sge0rnn0  46811  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem4  47041  ovnlecvr2  47053  hspmbllem2  47070  vonioo  47125  vonicc  47128  smflimsuplem1  47263  smflimsuplem2  47264  n0nsn2el  47488  clnbgrn0  48323  brgrici  48404  brgrilci  48496  cznrng  48752  lmodn0  48986  inisegn0a  49326  elfvne0  49339  lanrcl  50111  ranrcl  50112  rellan  50113  relran  50114  aacllem  50291  amgmw2d  50294