Theorem ne0i 4294

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960  ∅c0 4286

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3909  df-nul 4287

This theorem is used by:  ne0d  4295  ne0ii  4297  inelcm  4425  rzalALT  4458  2reu4  4487  tpnzd  4748  issn  4799  brne0  5163  ord0eln0  6421  elfvunirn  6915  elfvmptrab1  7022  elovmpt3imp  7673  onnmin  7799  f1oweALT  7971  brovpreldm  8086  bropopvvv  8087  frxp  8124  mpoxopxnop0  8213  brovex  8220  ord1eln01  8483  ord2eln012  8484  oe1m  8532  oa00  8546  oarec  8549  omord  8555  omeulem1  8569  oewordri  8580  oeordsuc  8582  oelim2  8583  nnmord  8620  map0g  8884  ixpn0  8930  unblem1  9255  wofib  9510  canthwdom  9544  inf1  9594  oemapvali  9656  cantnf  9665  epfrs  9703  acnrcl  10038  iunfictbso  10110  dfac5lem2  10120  kmlem6  10151  fin23lem40  10346  isf34lem7  10374  isf34lem6  10375  fin1a2lem7  10401  fin1a2lem13  10407  alephval2  10568  tskpr  10766  inar1  10771  tskuni  10779  tskxp  10783  tskmap  10784  grur1  10816  axgroth3  10827  inaprc  10832  addclpi  10888  indpi  10903  nqerf  10926  genpn0  10999  infrelb  12211  infssuzle  12966  eliooxr  13442  iccssioo2  13457  iccsupr  13480  elfzoel1  13697  elfzoel2  13698  fzon0  13718  fseqsupubi  14027  hashnn0n0nn  14440  pfxn0  14741  r19.2uz  15422  climuni  15622  ruclem11  16313  bezoutlem2  16615  lcmgcdlem  16681  prmreclem6  16998  vdwlem8  17065  ramtcl  17087  catcone0  17760  fpwipodrs  18613  gsumval2  18765  mgm2nsgrplem1  19003  sgrp2nmndlem1  19008  issubg3  19234  brgici  19364  odlem2  19632  gexlem2  19675  sylow3lem3  19722  abln0  19960  cyggexb  19992  gsumval3  20000  ablfacrp2  20162  ablfac1c  20166  pgpfaclem2  20177  ringn0  20419  brrici  20623  01eq0ringOLD  20658  subrgugrp  20719  brlmici  21219  mpllsslem  22178  ltbwe  22224  mpfrcl  22265  ply1plusgfvi  22430  ply1frcl  22507  cramerimplem2  22870  cramerimplem3  22871  cramerimp  22872  clsval2  23236  lmmo  23566  1stcfb  23631  2ndcsep  23645  ptclsg  23801  txindis  23820  hmphi  23963  trfbas2  24029  flimclslem  24170  ustfilxp  24399  prdsmet  24556  prdsbl  24677  tgioo  24982  caun0  25469  ovolctb  25678  mbflimsup  25854  itg1climres  25902  itg2i1fseq2  25944  dvferm1lem  26172  dvferm2lem  26174  dvferm  26176  c1liplem1  26184  dvivthlem1  26196  aalioulem2  26525  birthdaylem1  27145  ltsval2  27849  nobdaymin  27975  tgldimor  28800  perpin  29034  axlowdimlem13  29333  uvtx01vtx  29776  wlkreslem  30046  wspniunwspnon  30301  usgr2wspthons3  30345  rusgrnumwwlks  30355  rusgrnumwwlk  30356  frgr2wwlkn0  30708  numclwwlk1  30741  numclwlk1lem1  30749  numclwwlk3  30765  numclwwlk5  30768  ubthlem1  31251  n0nsnel  32890  eldmne0  33001  drgextlsp  34007  dimval  34014  dimvalfi  34015  zarcls1  34282  rge0scvg  34362  qqhucn  34405  voliune  34643  eulerpartlemt  34785  dfscott3  35529  erdszelem2  35697  dfso3  36225  fnemeet1  36910  fnejoin1  36912  tailfb  36921  ttc0elw  37071  ttc0el  37079  curfv  38284  ptrecube  38304  poimirlem23  38327  poimirlem31  38335  poimirlem32  38336  mblfinlem2  38342  ismblfin  38345  ovoliunnfl  38346  voliunnfl  38348  itg2addnc  38358  totbndbnd  38473  prdsbnd  38477  heibor1lem  38493  eldisjdmqsim  39499  prtlem100  39666  prter3  39689  ishlat3N  40161  hlsupr2  40194  elpaddri  40609  diaintclN  41865  dibintclN  41974  dihintcl  42151  unitscyglem4  42998  rencldnfi  43581  omlimcl2  44002  oaun3lem1  44134  neik0imk0p  44795  clsk3nimkb  44799  amgm3d  44958  amgm4d  44959  prmunb2  45054  rzalf  45770  pwfin0  45815  ssuzfz  46098  fsumiunss  46324  limsupvaluz2  46485  supcnvlimsup  46487  jumpncnp  46645  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  stoweidlem11  46758  stoweidlem31  46778  stoweidlem34  46781  stoweidlem59  46806  fourierdlem31  46885  fourierdlem42  46896  fourierdlem64  46917  fourierdlem73  46926  fourierdlem79  46932  qndenserrnbllem  47041  qndenserrn  47046  sge0rnn0  47115  hoidmvlelem1  47342  hoidmvlelem2  47343  hoidmvlelem4  47345  ovnlecvr2  47357  hspmbllem2  47374  vonioo  47429  vonicc  47432  smflimsuplem1  47567  smflimsuplem2  47568  n0nsn2el  47795  clnbgrn0  48630  brgrici  48711  brgrilci  48803  cznrng  49059  lmodn0  49308  inisegn0a  49647  elfvne0  49660  lanrcl  50432  ranrcl  50433  rellan  50434  relran  50435  aacllem  50654  amgmw2d  50685