Theorem ne0i 3921

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

Assertion

Ref	Expression
ne0i	|- ( B e. A -> A =/= (/) )

Proof of Theorem ne0i

Step	Hyp	Ref	Expression
1		n0i 3920	. 2 |- ( B e. A -> -. A = (/) )
2	1	neqned 2801	1 |- ( B e. A -> A =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1990   =/= wne 2794   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  ne0ii  3923  inelcm  4032  rzal  4073  rexn0  4074  snnzg  4308  prnzg  4311  tpnzd  4314  issn  4363  brne0  4702  exss  4931  ord0eln0  5779  elfvdm  6220  elfvmptrab1  6305  isofrlem  6590  elovmpt3imp  6890  onnmin  7003  f1oweALT  7152  brovpreldm  7254  bropopvvv  7255  frxp  7287  mpt2xopxnop0  7341  brovex  7348  fvmpt2curryd  7397  onnseq  7441  oe1m  7625  oa00  7639  oarec  7642  omord  7648  oewordri  7672  oeordsuc  7674  oelim2  7675  oeoalem  7676  oeoelem  7678  oeeui  7682  nnmord  7712  nnawordex  7717  map0g  7897  ixpn0  7940  omxpenlem  8061  frfi  8205  unblem1  8212  supgtoreq  8376  infltoreq  8408  wofib  8450  canthwdom  8484  inf1  8519  oemapvali  8581  cantnflem1a  8582  cantnflem1d  8585  cantnflem1  8586  cantnf  8590  epfrs  8607  acnrcl  8865  iunfictbso  8937  dfac5lem2  8947  dfac9  8958  kmlem6  8977  fin23lem40  9173  isf34lem7  9201  isf34lem6  9202  fin1a2lem7  9228  fin1a2lem13  9234  axdc3lem4  9275  alephval2  9394  intwun  9557  r1limwun  9558  tskpr  9592  inar1  9597  tskuni  9605  tskxp  9609  tskmap  9610  gruina  9640  grur1a  9641  grur1  9642  axgroth3  9653  inaprc  9658  addclpi  9714  mulclpi  9715  indpi  9729  nqerf  9752  genpn0  9825  supsrlem  9932  axpre-sup  9990  infrelb  11008  supfirege  11009  uzn0  11703  infssuzle  11771  suprzub  11779  eliooxr  12232  iccssioo2  12246  iccsupr  12266  fzn0  12355  elfzoel1  12468  elfzoel2  12469  fzon0  12487  flval3  12616  icopnfsup  12664  fseqsupubi  12777  hashnn0n0nn  13180  swrdn0  13430  dfrtrcl2  13802  sqrlem3  13985  r19.2uz  14091  climuni  14283  isercolllem2  14396  isercolllem3  14397  climsup  14400  mertenslem2  14617  ruclem11  14969  gcdcllem1  15221  bezoutlem2  15257  lcmgcdlem  15319  pclem  15543  prmreclem1  15620  prmreclem6  15625  4sqlem13  15661  vdwmc2  15683  vdwlem6  15690  vdwlem8  15692  vdwnnlem3  15701  ramtcl  15714  prmgaplem3  15757  prmgaplem4  15758  mrcflem  16266  mrcval  16270  iscatd2  16342  fpwipodrs  17164  gsumval2  17280  mgm2nsgrplem1  17405  sgrp2nmndlem1  17410  grpbn0  17451  issubgrpd2  17610  issubg3  17612  issubg4  17613  subgint  17618  cycsubgcl  17620  nmzsubg  17635  ghmpreima  17682  brgici  17712  gastacl  17742  odlem2  17958  gexlem2  17997  sylow1lem5  18017  pgpssslw  18029  sylow2alem2  18033  sylow2blem3  18037  fislw  18040  sylow3lem3  18044  sylow3lem4  18045  torsubg  18257  oddvdssubg  18258  abln0  18270  iscygd  18289  iscygodd  18290  cyggexb  18300  gsumval3  18308  dprdsubg  18423  ablfacrp2  18466  ablfac1c  18470  ablfac1eu  18472  pgpfaclem2  18481  ringn0  18603  subrgugrp  18799  cntzsubr  18812  islss4  18962  lss1d  18963  lssintcl  18964  brlmici  19069  lspsolvlem  19142  lbsextlem1  19158  lidlsubg  19215  01eq0ring  19272  abvn0b  19302  psrbas  19378  mplsubglem  19434  mpllsslem  19435  ltbwe  19472  mplind  19502  mpfrcl  19518  ply1plusgfvi  19612  ply1frcl  19683  zringlpirlem1  19832  ocvlss  20016  lmiclbs  20176  lmisfree  20181  mat1ric  20293  dmatsgrp  20305  scmatsgrp  20325  scmatsgrp1  20328  scmatlss  20331  scmatric  20343  cramerimplem2  20490  cramerimplem3  20491  cramerimp  20492  cpmatsubgpmat  20525  matcpmric  20564  pmmpric  20628  clscld  20851  clsval2  20854  lmmo  21184  1stcfb  21248  2ndcdisj  21259  2ndcsep  21262  ptclsg  21418  dfac14lem  21420  txindis  21437  hmphi  21580  opnfbas  21646  trfbas2  21647  isfil2  21660  filn0  21666  filssufilg  21715  rnelfmlem  21756  flimclslem  21788  flimfnfcls  21832  ptcmplem2  21857  clssubg  21912  tgpconncomp  21916  tsmsfbas  21931  ustfilxp  22016  ustne0  22017  prdsmet  22175  xbln0  22219  bln0  22220  prdsbl  22296  metustfbas  22362  metustbl  22371  nrgdomn  22475  tgioo  22599  icccmplem2  22626  icccmplem3  22627  reconnlem2  22630  phtpcer  22794  phtpcerOLD  22795  reparpht  22798  phtpcco2  22799  pcohtpy  22820  pcorevlem  22826  isclmp  22897  caun0  23079  iscmet3lem2  23090  bcthlem4  23124  minveclem3b  23199  ivthlem2  23221  ivthlem3  23222  evthicc  23228  ovollb2  23257  ovolctb  23258  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliun2  23274  ioombl1lem4  23329  uniioombllem1  23349  uniioombllem2  23351  uniioombllem6  23356  mbfsup  23431  mbfinf  23432  mbflimsup  23433  itg1climres  23481  itg2monolem1  23517  itg2mono  23520  itg2i1fseq2  23523  dvferm1lem  23747  dvferm2lem  23749  dvferm  23751  c1liplem1  23759  dvivthlem1  23771  aalioulem2  24088  ulm0  24145  pilem2  24206  pilem3  24207  birthdaylem1  24678  ftalem3  24801  ftalem4  24802  ftalem5  24803  dchrabs  24985  pntlem3  25298  tgldimor  25397  tglnne0  25535  axlowdimlem13  25834  axlowdim1  25839  uvtxa01vtx0  26297  wlkreslem  26566  wspniunwspnon  26819  usgr2wspthons3  26857  rusgrnumwwlks  26869  rusgrnumwwlk  26870  frgr2wwlkn0  27192  numclwwlk1  27231  numclwwlk3OLD  27242  numclwwlk3  27243  numclwwlk5  27246  nvo00  27616  nmorepnf  27623  ubthlem1  27726  minvecolem1  27730  submomnd  29710  slmdbn0  29761  slmdsn0  29764  suborng  29815  ordtconnlem1  29970  rge0scvg  29995  qqhucn  30036  rrhre  30065  sigagenval  30203  voliune  30292  oddpwdc  30416  eulerpartlemt  30433  bnj1177  31074  bnj1523  31139  erdszelem2  31174  erdszelem8  31180  txsconnlem  31222  cvxsconn  31225  cvmsss2  31256  cvmliftmolem2  31264  cvmlift2lem12  31296  cvmliftpht  31300  dfso3  31601  sltval2  31809  nocvxminlem  31893  finminlem  32312  fnemeet1  32361  fnejoin1  32363  tailfb  32372  onint1  32448  finxpreclem4  33231  curfv  33389  ptrecube  33409  poimirlem23  33432  poimirlem31  33440  poimirlem32  33441  heicant  33444  mblfinlem2  33447  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  itg2addnc  33464  ftc1anclem7  33491  ftc1anc  33493  totbndbnd  33588  prdsbnd  33592  prdsbnd2  33594  heibor1lem  33608  prtlem100  34144  prter3  34167  lkrlss  34382  ishlat3N  34641  hlsupr2  34673  elpaddri  35088  pclvalN  35176  dian0  36328  diaintclN  36347  docaclN  36413  dibintclN  36456  dicn0  36481  dihglblem5  36587  dihglb2  36631  dihintcl  36633  doch2val2  36653  dochocss  36655  lclkr  36822  lclkrs  36828  lcfr  36874  nacsfix  37275  mzpcln0  37291  rencldnfilem  37384  rencldnfi  37385  fnwe2lem2  37621  kelac1  37633  harn0  37672  hbtlem2  37694  neik0imk0p  38334  clsk3nimkb  38338  gneispa  38428  amgm3d  38502  amgm4d  38503  prmunb2  38510  rzalf  39176  ubelsupr  39179  pwfin0  39231  ne0d  39308  suprnmpt  39355  disjinfi  39380  mapdm0OLD  39383  suprubrnmpt2  39467  suprubrnmpt  39468  ssfiunibd  39523  ssuzfz  39565  allbutfi  39616  allbutfiinf  39647  fsumiunss  39807  climinf  39838  limclr  39887  limsupubuzlem  39944  limsupvaluz2  39970  supcnvlimsup  39972  liminflelimsupuz  40017  jumpncnp  40111  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc1  40148  ioodvbdlimc2lem  40149  ioodvbdlimc2  40150  stoweidlem11  40228  stoweidlem31  40248  stoweidlem34  40251  stoweidlem36  40253  stoweidlem59  40276  fourierdlem20  40344  fourierdlem25  40349  fourierdlem31  40355  fourierdlem37  40361  fourierdlem42  40366  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem52  40375  fourierdlem54  40377  fourierdlem64  40387  fourierdlem73  40396  fourierdlem79  40402  fouriercn  40449  elaa2lem  40450  qndenserrnbllem  40514  qndenserrn  40519  salgenval  40541  salgenn0  40549  sge0rnn0  40585  sge0isum  40644  sge0reuzb  40665  ovnlerp  40776  ovnf  40777  hsphoidmvle2  40799  hsphoidmvle  40800  hoiprodp1  40802  hoidmv1lelem1  40805  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem4  40812  ovnlecvr2  40824  hoidifhspdmvle  40834  hspmbllem1  40840  hspmbllem2  40841  hspmbllem3  40842  ovnovollem2  40871  vonioo  40896  vonicc  40899  smflimlem1  40979  smflimsuplem1  41026  smflimsuplem2  41027  smflimsuplem5  41030  smflimsuplem7  41032  2reu4  41190  cznrng  41955  lincolss  42223  lmodn0  42284  aacllem  42547  amgmw2d  42550