Theorem ne0i 3773

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 3772	. 2 |- ( B e. A -> -. A = (/) )
2	1	neqned 2634	1 |- ( B e. A -> A =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1870   =/= wne 2625   (/)c0 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-v 3089  df-dif 3445  df-nul 3768

This theorem is referenced by:  ne0ii  3774  inelcm  3853  rzal  3905  rexn0  3906  snnzg  4120  tpnzd  4125  brne0  4473  exss  4685  ord0eln0  5496  elfvdm  5907  elfvmptrab1  5986  isofrlem  6246  elovmpt3imp  6538  onnmin  6644  f1oweALT  6791  bropopvvv  6887  frxp  6917  mpt2xopxnop0  6969  brovex  6976  fvmpt2curryd  7026  onnseq  7071  oe1m  7254  oa00  7268  oarec  7271  omord  7277  oewordri  7301  oeordsuc  7303  oelim2  7304  oeoalem  7305  oeoelem  7307  oeeui  7311  nnmord  7341  nnawordex  7346  map0g  7519  ixpn0  7562  omxpenlem  7679  frfi  7822  unblem1  7829  supgtoreq  7992  infltoreq  8018  wofib  8060  canthwdom  8094  inf1  8127  oemapvali  8188  cantnflem1a  8189  cantnflem1d  8192  cantnflem1  8193  cantnf  8197  epfrs  8214  acnrcl  8471  iunfictbso  8543  dfac5lem2  8553  dfac9  8564  kmlem6  8583  fin23lem40  8779  isf34lem7  8807  isf34lem6  8808  fin1a2lem7  8834  fin1a2lem13  8840  axdc3lem4  8881  alephval2  8995  intwun  9159  r1limwun  9160  tskpr  9194  inar1  9199  tskuni  9207  tskxp  9211  tskmap  9212  gruina  9242  grur1a  9243  grur1  9244  axgroth3  9255  inaprc  9260  addclpi  9316  mulclpi  9317  indpi  9331  nqerf  9354  genpn0  9427  supsrlem  9534  axpre-sup  9592  infmrclOLD  10593  infrelb  10596  infmrlbOLD  10597  supfirege  10598  uzn0  11174  infssuzle  11244  infmssuzleOLD  11246  suprzub  11255  eliooxr  11693  iccssioo2  11707  iccsupr  11727  fzn0  11811  elfzoel1  11916  elfzoel2  11917  fzon0  11935  flval3  12047  icopnfsup  12089  fseqsupubi  12188  hashnn0n0nn  12567  swrdn0  12771  dfrtrcl2  13104  sqrlem3  13287  r19.2uz  13393  climuni  13594  isercolllem2  13707  isercolllem3  13708  climsup  13711  mertenslem2  13919  ruclem11  14270  gcdcllem1  14447  bezoutlem2  14478  lcmgcdlem  14542  pclem  14751  prmreclem1  14823  prmreclem6  14828  4sqlem13OLD  14864  4sqlem13  14870  vdwmc2  14892  vdwlem6  14899  vdwlem8  14901  vdwnnlem3  14910  ramtcl  14927  ramtclOLD  14928  prmgaplem3  14986  prmgaplem4  14987  mrcflem  15463  mrcval  15467  iscatd2  15538  fpwipodrs  16361  gsumval2  16474  mgm2nsgrplem1  16603  sgrp2nmndlem1  16608  grpbn0  16646  issubgrpd2  16784  issubg3  16786  issubg4  16787  subgint  16792  cycsubgcl  16794  nmzsubg  16809  ghmpreima  16855  brgici  16885  gastacl  16914  odlem2  17130  gexlem2  17169  sylow1lem5  17189  pgpssslw  17201  sylow2alem2  17205  sylow2blem3  17209  fislw  17212  sylow3lem3  17216  sylow3lem4  17217  torsubg  17427  oddvdssubg  17428  abln0  17440  iscygd  17457  iscygodd  17458  cyggexb  17468  gsumval3  17476  dprdsubg  17592  ablfacrp2  17635  ablfac1c  17639  ablfac1eu  17641  pgpfaclem2  17650  ringn0  17766  subrgugrp  17962  cntzsubr  17975  islss4  18120  lss1d  18121  lssintcl  18122  brlmici  18227  lspsolvlem  18300  lbsextlem1  18316  lidlsubg  18373  01eq0ring  18431  abvn0b  18461  psrbas  18537  mplsubglem  18593  mpllsslem  18594  ltbwe  18631  mplind  18660  mpfrcl  18676  ply1plusgfvi  18770  ply1frcl  18842  zringlpirlem1  18987  ocvlss  19166  lmiclbs  19326  lmisfree  19331  mat1ric  19443  dmatsgrp  19455  scmatsgrp  19475  scmatsgrp1  19478  scmatlss  19481  scmatric  19493  cramerimplem2  19640  cramerimplem3  19641  cramerimp  19642  cpmatsubgpmat  19675  matcpmric  19714  pmmpric  19778  clscld  19993  clsval2  19996  lmmo  20327  1stcfb  20391  2ndcdisj  20402  2ndcsep  20405  ptclsg  20561  dfac14lem  20563  txindis  20580  hmphi  20723  opnfbas  20788  trfbas2  20789  isfil2  20802  filn0  20808  filssufilg  20857  rnelfmlem  20898  flimclslem  20930  flimfnfcls  20974  ptcmplem2  20999  clssubg  21054  tgpconcomp  21058  tsmsfbas  21073  ustfilxp  21158  ustne0  21159  prdsmet  21316  xbln0  21360  bln0  21361  prdsbl  21437  metustfbas  21503  metustbl  21512  nrgdomn  21605  tgioo  21725  icccmplem2  21752  icccmplem3  21753  reconnlem2  21756  phtpcer  21919  reparpht  21922  phtpcco2  21923  pcohtpy  21944  pcorevlem  21950  caun0  22144  iscmet3lem2  22155  bcthlem4  22188  minveclem3b  22263  ivthlem2  22284  ivthlem3  22285  evthicc  22291  ovollb2  22320  ovolctb  22321  ovolunlem1a  22327  ovolunlem1  22328  ovoliunlem1  22333  ovoliun2  22337  ioombl1lem4  22391  uniioombllem1  22415  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem6  22423  mbfsup  22497  mbfinf  22498  mbfinfOLD  22499  mbflimsup  22500  mbflimsupOLD  22501  itg1climres  22549  itg2monolem1  22585  itg2mono  22588  itg2i1fseq2  22591  dvferm1lem  22813  dvferm2lem  22815  dvferm  22817  c1liplem1  22825  dvivthlem1  22837  aalioulem2  23154  ulm0  23211  pilem2  23272  pilem2OLD  23273  pilem3  23274  pilem3OLD  23275  birthdaylem1  23742  ftalem3  23864  ftalem4  23865  ftalem5  23866  dchrabs  24051  pntlem3  24310  tgldimor  24409  tglnne0  24544  axlowdimlem13  24830  axlowdim1  24835  clwwlknprop  25345  2wlkonot3v  25448  2spthonot3v  25449  usg2spthonot  25461  usg2spthonot0  25462  2spot2iun2spont  25464  frg2wotn0  25629  ghgrpOLD  25941  nvo00  26247  nmorepnf  26254  ubthlem1  26357  minvecolem1  26361  submomnd  28311  slmdbn0  28362  slmdsn0  28365  suborng  28417  ordtconlem1  28569  rge0scvg  28594  qqhucn  28635  rrhre  28664  sigagenval  28801  voliune  28891  oddpwdc  29013  eulerpartlemt  29030  bnj1177  29603  bnj1523  29668  erdszelem2  29703  erdszelem8  29709  txsconlem  29751  cvxscon  29754  cvmsss2  29785  cvmliftmolem2  29793  cvmlift2lem12  29825  cvmliftpht  29829  dfso3  30140  sltval2  30330  nocvxminlem  30364  nobndlem5  30370  finminlem  30759  fnemeet1  30807  fnejoin1  30809  tailfb  30818  onint1  30894  ptrecube  31643  poimirlem23  31666  poimirlem31  31674  poimirlem32  31675  heicant  31678  mblfinlem2  31681  ismblfin  31684  ovoliunnfl  31685  voliunnfl  31687  itg2addnc  31699  ftc1anclem7  31726  ftc1anc  31728  totbndbnd  31824  prdsbnd  31828  prdsbnd2  31830  heibor1lem  31844  prtlem100  32134  prter3  32161  lkrlss  32369  ishlat3N  32628  hlsupr2  32660  elpaddri  33075  pclvalN  33163  dian0  34315  diaintclN  34334  docaclN  34400  dibintclN  34443  dicn0  34468  dihglblem5  34574  dihglb2  34618  dihintcl  34620  doch2val2  34640  dochocss  34642  lclkr  34809  lclkrs  34815  lcfr  34861  nacsfix  35262  mzpcln0  35278  rencldnfilem  35371  rencldnfi  35372  fnwe2lem2  35614  kelac1  35626  harn0  35666  hbtlem2  35688  amgm3d  36287  amgm4d  36288  prmunb2  36295  rzalf  36977  ubelsupr  36980  pwfin0  37044  suprnmpt  37060  disjinfi  37090  ssfiunibd  37135  fsumiunss  37228  climinf  37255  climinfOLD  37256  limclr  37307  jumpncnp  37347  ioodvbdlimc1lem1  37374  ioodvbdlimc1lem2  37375  ioodvbdlimc1  37376  ioodvbdlimc2lem  37377  ioodvbdlimc2  37378  stoweidlem11  37439  stoweidlem31  37460  stoweidlem34  37463  stoweidlem36  37465  stoweidlem59  37488  fourierdlem20  37557  fourierdlem25  37562  fourierdlem31  37568  fourierdlem37  37574  fourierdlem42  37579  fourierdlem46  37583  fourierdlem48  37585  fourierdlem49  37586  fourierdlem52  37589  fourierdlem54  37591  fourierdlem64  37601  fourierdlem73  37610  fourierdlem79  37616  fouriercn  37663  elaa2lem  37664  salgenval  37728  salgencl  37736  sge0rnn0  37743  2reu4  38001  cznrng  38714  lincolss  38986  lmodn0  39047  aacllem  39300