Theorem ne0i 4265

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2942  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-dif 3886  df-nul 4254

This theorem is referenced by:  ne0d  4266  ne0ii  4268  inelcm  4395  rzalALT  4437  rexn0OLD  4442  2reu4  4454  tpnzd  4713  issn  4760  brne0  5120  ord0eln0  6305  elfvmptrab1  6884  elovmpt3imp  7504  onnmin  7625  f1oweALT  7788  brovpreldm  7900  bropopvvv  7901  frxp  7938  mpoxopxnop0  8002  brovex  8009  oe1m  8338  oa00  8352  oarec  8355  omord  8361  omeulem1  8375  oewordri  8385  oeordsuc  8387  oelim2  8388  nnmord  8425  map0g  8630  ixpn0  8676  unblem1  8996  wofib  9234  canthwdom  9268  inf1  9310  oemapvali  9372  cantnf  9381  epfrs  9420  acnrcl  9729  iunfictbso  9801  dfac5lem2  9811  kmlem6  9842  fin23lem40  10038  isf34lem7  10066  isf34lem6  10067  fin1a2lem7  10093  fin1a2lem13  10099  alephval2  10259  tskpr  10457  inar1  10462  tskuni  10470  tskxp  10474  tskmap  10475  grur1  10507  axgroth3  10518  inaprc  10523  addclpi  10579  indpi  10594  nqerf  10617  genpn0  10690  infrelb  11890  infssuzle  12600  eliooxr  13066  iccssioo2  13081  iccsupr  13103  elfzoel1  13314  elfzoel2  13315  fzon0  13333  fseqsupubi  13626  hashnn0n0nn  14034  pfxn0  14327  r19.2uz  14991  climuni  15189  ruclem11  15877  bezoutlem2  16176  lcmgcdlem  16239  prmreclem6  16550  vdwlem8  16617  ramtcl  16639  catcone0  17313  fpwipodrs  18173  gsumval2  18285  mgm2nsgrplem1  18472  sgrp2nmndlem1  18477  issubg3  18688  brgici  18801  odlem2  19062  gexlem2  19102  sylow3lem3  19149  abln0  19383  cyggexb  19415  gsumval3  19423  ablfacrp2  19585  ablfac1c  19589  pgpfaclem2  19600  ringn0  19757  subrgugrp  19958  brlmici  20246  01eq0ring  20456  mpllsslem  21116  ltbwe  21155  mpfrcl  21205  ply1plusgfvi  21323  ply1frcl  21394  cramerimplem2  21741  cramerimplem3  21742  cramerimp  21743  clsval2  22109  lmmo  22439  1stcfb  22504  2ndcsep  22518  ptclsg  22674  txindis  22693  hmphi  22836  trfbas2  22902  flimclslem  23043  ustfilxp  23272  prdsmet  23431  prdsbl  23553  tgioo  23865  caun0  24350  ovolctb  24559  mbflimsup  24735  itg1climres  24784  itg2i1fseq2  24826  dvferm1lem  25053  dvferm2lem  25055  dvferm  25057  c1liplem1  25065  dvivthlem1  25077  aalioulem2  25398  birthdaylem1  26006  tgldimor  26767  axlowdimlem13  27225  uvtx01vtx  27667  wlkreslem  27939  wspniunwspnon  28189  usgr2wspthons3  28230  rusgrnumwwlks  28240  rusgrnumwwlk  28241  frgr2wwlkn0  28593  numclwwlk1  28626  numclwlk1lem1  28634  numclwwlk3  28650  numclwwlk5  28653  ubthlem1  29133  eldmne0  30864  drgextlsp  31583  dimval  31588  dimvalfi  31589  zarcls1  31721  rge0scvg  31801  qqhucn  31842  voliune  32097  eulerpartlemt  32238  erdszelem2  33054  dfso3  33566  sltval2  33786  fnemeet1  34482  fnejoin1  34484  tailfb  34493  curfv  35684  ptrecube  35704  poimirlem23  35727  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  ismblfin  35745  ovoliunnfl  35746  voliunnfl  35748  itg2addnc  35758  totbndbnd  35874  prdsbnd  35878  heibor1lem  35894  prtlem100  36800  prter3  36823  ishlat3N  37295  hlsupr2  37328  elpaddri  37743  diaintclN  38999  dibintclN  39108  dihintcl  39285  rencldnfi  40559  neik0imk0p  41535  clsk3nimkb  41539  amgm3d  41699  amgm4d  41700  prmunb2  41818  rzalf  42449  pwfin0  42499  ssuzfz  42778  fsumiunss  43006  limsupvaluz2  43169  supcnvlimsup  43171  jumpncnp  43329  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem11  43442  stoweidlem31  43462  stoweidlem34  43465  stoweidlem59  43490  fourierdlem31  43569  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem64  43601  fourierdlem73  43610  fourierdlem79  43616  qndenserrnbllem  43725  qndenserrn  43730  sge0rnn0  43796  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem4  44026  ovnlecvr2  44038  hspmbllem2  44055  vonioo  44110  vonicc  44113  smflimsuplem1  44240  smflimsuplem2  44241  cznrng  45401  lmodn0  45724  elfvne0  46064  aacllem  46391  amgmw2d  46394