Theorem ne0i 3705

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

Syntax hints:   -> wi 4   e. wcel 1891   =/= wne 2622   (/)c0 3699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-v 3015  df-dif 3375  df-nul 3700

This theorem is referenced by:  ne0ii  3706  inelcm  3787  rzal  3839  rexn0  3840  snnzg  4058  tpnzd  4063  brne0  4422  exss  4636  ord0eln0  5456  elfvdm  5874  elfvmptrab1  5954  isofrlem  6217  elovmpt3imp  6512  onnmin  6618  f1oweALT  6765  brovpreldm  6861  bropopvvv  6862  frxp  6894  mpt2xopxnop0  6949  brovex  6956  fvmpt2curryd  7005  onnseq  7050  oe1m  7233  oa00  7247  oarec  7250  omord  7256  oewordri  7280  oeordsuc  7282  oelim2  7283  oeoalem  7284  oeoelem  7286  oeeui  7290  nnmord  7320  nnawordex  7325  map0g  7498  ixpn0  7541  omxpenlem  7660  frfi  7803  unblem1  7810  supgtoreq  7973  infltoreq  8005  wofib  8047  canthwdom  8081  inf1  8114  oemapvali  8176  cantnflem1a  8177  cantnflem1d  8180  cantnflem1  8181  cantnf  8185  epfrs  8202  acnrcl  8460  iunfictbso  8532  dfac5lem2  8542  dfac9  8553  kmlem6  8572  fin23lem40  8768  isf34lem7  8796  isf34lem6  8797  fin1a2lem7  8823  fin1a2lem13  8829  axdc3lem4  8870  alephval2  8984  intwun  9147  r1limwun  9148  tskpr  9182  inar1  9187  tskuni  9195  tskxp  9199  tskmap  9200  gruina  9230  grur1a  9231  grur1  9232  axgroth3  9243  inaprc  9248  addclpi  9304  mulclpi  9305  indpi  9319  nqerf  9342  genpn0  9415  supsrlem  9522  axpre-sup  9580  infmrclOLD  10582  infrelb  10585  infmrlbOLD  10586  supfirege  10587  uzn0  11164  infssuzle  11234  infmssuzleOLD  11236  suprzub  11245  eliooxr  11683  iccssioo2  11697  iccsupr  11717  fzn0  11804  elfzoel1  11911  elfzoel2  11912  fzon0  11930  flval3  12044  icopnfsup  12086  fseqsupubi  12185  hashnn0n0nn  12564  swrdn0  12785  dfrtrcl2  13136  sqrlem3  13319  r19.2uz  13425  climuni  13627  isercolllem2  13740  isercolllem3  13741  climsup  13744  mertenslem2  13952  ruclem11  14303  gcdcllem1  14484  bezoutlem2OLD  14515  bezoutlem2  14518  lcmgcdlem  14582  pclem  14799  prmreclem1  14871  prmreclem6  14876  4sqlem13OLD  14912  4sqlem13  14918  vdwmc2  14940  vdwlem6  14947  vdwlem8  14949  vdwnnlem3  14958  ramtcl  14975  ramtclOLD  14976  prmgaplem3  15034  prmgaplem4  15035  mrcflem  15523  mrcval  15527  iscatd2  15598  fpwipodrs  16421  gsumval2  16534  mgm2nsgrplem1  16663  sgrp2nmndlem1  16668  grpbn0  16706  issubgrpd2  16844  issubg3  16846  issubg4  16847  subgint  16852  cycsubgcl  16854  nmzsubg  16869  ghmpreima  16915  brgici  16945  gastacl  16974  odlem2  17199  odlem2OLD  17215  gexlem2  17244  gexlem2OLD  17247  sylow1lem5  17265  pgpssslw  17277  sylow2alem2  17281  sylow2blem3  17285  fislw  17288  sylow3lem3  17292  sylow3lem4  17293  torsubg  17503  oddvdssubg  17504  abln0  17516  iscygd  17533  iscygodd  17534  cyggexb  17544  gsumval3  17552  dprdsubg  17668  ablfacrp2  17711  ablfac1c  17715  ablfac1eu  17717  pgpfaclem2  17726  ringn0  17842  subrgugrp  18038  cntzsubr  18051  islss4  18196  lss1d  18197  lssintcl  18198  brlmici  18303  lspsolvlem  18376  lbsextlem1  18392  lidlsubg  18449  01eq0ring  18507  abvn0b  18537  psrbas  18613  mplsubglem  18669  mpllsslem  18670  ltbwe  18707  mplind  18736  mpfrcl  18752  ply1plusgfvi  18846  ply1frcl  18918  zringlpirlem1  19064  ocvlss  19246  lmiclbs  19406  lmisfree  19411  mat1ric  19523  dmatsgrp  19535  scmatsgrp  19555  scmatsgrp1  19558  scmatlss  19561  scmatric  19573  cramerimplem2  19720  cramerimplem3  19721  cramerimp  19722  cpmatsubgpmat  19755  matcpmric  19794  pmmpric  19858  clscld  20073  clsval2  20076  lmmo  20407  1stcfb  20471  2ndcdisj  20482  2ndcsep  20485  ptclsg  20641  dfac14lem  20643  txindis  20660  hmphi  20803  opnfbas  20868  trfbas2  20869  isfil2  20882  filn0  20888  filssufilg  20937  rnelfmlem  20978  flimclslem  21010  flimfnfcls  21054  ptcmplem2  21079  clssubg  21134  tgpconcomp  21138  tsmsfbas  21153  ustfilxp  21238  ustne0  21239  prdsmet  21396  xbln0  21440  bln0  21441  prdsbl  21517  metustfbas  21583  metustbl  21592  nrgdomn  21685  tgioo  21825  icccmplem2  21852  icccmplem3  21853  reconnlem2  21856  phtpcer  22037  reparpht  22040  phtpcco2  22041  pcohtpy  22062  pcorevlem  22068  caun0  22262  iscmet3lem2  22273  bcthlem4  22306  minveclem3b  22381  minveclem3bOLD  22393  ivthlem2  22414  ivthlem3  22415  evthicc  22421  ovollb2  22453  ovolctb  22454  ovolunlem1a  22460  ovolunlem1  22461  ovoliunlem1  22466  ovoliun2  22470  ioombl1lem4  22526  uniioombllem1  22550  uniioombllem2  22552  uniioombllem2OLD  22553  uniioombllem6  22558  mbfsup  22632  mbfinf  22633  mbfinfOLD  22634  mbflimsup  22635  mbflimsupOLD  22636  itg1climres  22684  itg2monolem1  22720  itg2mono  22723  itg2i1fseq2  22726  dvferm1lem  22948  dvferm2lem  22950  dvferm  22952  c1liplem1  22960  dvivthlem1  22972  aalioulem2  23301  ulm0  23358  pilem2  23419  pilem2OLD  23420  pilem3  23421  pilem3OLD  23422  birthdaylem1  23889  ftalem3  24011  ftalem4  24012  ftalem5  24013  ftalem4OLD  24014  ftalem5OLD  24015  dchrabs  24200  pntlem3  24459  tgldimor  24558  tglnne0  24697  axlowdimlem13  24996  axlowdim1  25001  clwwlknprop  25512  2wlkonot3v  25615  2spthonot3v  25616  usg2spthonot  25628  usg2spthonot0  25629  2spot2iun2spont  25631  frg2wotn0  25796  ghgrpOLD  26108  nvo00  26414  nmorepnf  26421  ubthlem1  26524  minvecolem1  26528  submomnd  28480  slmdbn0  28531  slmdsn0  28534  suborng  28585  ordtconlem1  28737  rge0scvg  28762  qqhucn  28803  rrhre  28832  sigagenval  28969  voliune  29058  oddpwdc  29193  eulerpartlemt  29210  bnj1177  29821  bnj1523  29886  erdszelem2  29921  erdszelem8  29927  txsconlem  29969  cvxscon  29972  cvmsss2  30003  cvmliftmolem2  30011  cvmlift2lem12  30043  cvmliftpht  30047  dfso3  30358  sltval2  30549  nocvxminlem  30585  nobndlem5  30591  finminlem  30980  fnemeet1  31028  fnejoin1  31030  tailfb  31039  onint1  31115  finxpreclem4  31788  ptrecube  31942  poimirlem23  31965  poimirlem31  31973  poimirlem32  31974  heicant  31977  mblfinlem2  31980  ismblfin  31983  ovoliunnfl  31984  voliunnfl  31986  itg2addnc  31998  ftc1anclem7  32025  ftc1anc  32027  totbndbnd  32123  prdsbnd  32127  prdsbnd2  32129  heibor1lem  32143  prtlem100  32431  prter3  32456  lkrlss  32663  ishlat3N  32922  hlsupr2  32954  elpaddri  33369  pclvalN  33457  dian0  34609  diaintclN  34628  docaclN  34694  dibintclN  34737  dicn0  34762  dihglblem5  34868  dihglb2  34912  dihintcl  34914  doch2val2  34934  dochocss  34936  lclkr  35103  lclkrs  35109  lcfr  35155  nacsfix  35556  mzpcln0  35572  rencldnfilem  35665  rencldnfi  35666  fnwe2lem2  35911  kelac1  35923  harn0  35963  hbtlem2  35985  amgm3d  36652  amgm4d  36653  prmunb2  36660  rzalf  37335  ubelsupr  37338  pwfin0  37398  suprnmpt  37449  disjinfi  37478  mapdm0  37481  ssfiunibd  37558  ssuzfz  37603  fsumiunss  37695  climinf  37726  climinfOLD  37727  limclr  37778  jumpncnp  37818  ioodvbdlimc1lem1  37845  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem1OLD  37847  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc1  37849  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  ioodvbdlimc2  37852  stoweidlem11  37928  stoweidlem31  37949  stoweidlem34  37952  stoweidlem36  37954  stoweidlem59  37977  fourierdlem20  38046  fourierdlem25  38051  fourierdlem31  38057  fourierdlem31OLD  38058  fourierdlem37  38064  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem46  38073  fourierdlem48  38075  fourierdlem49  38076  fourierdlem52  38079  fourierdlem54  38081  fourierdlem64  38091  fourierdlem73  38100  fourierdlem79  38106  fouriercn  38153  elaa2lem  38154  elaa2lemOLD  38155  qndenserrnbllem  38220  qndenserrn  38225  salgenval  38239  salgenn0  38247  sge0rnn0  38269  sge0isum  38328  ovnlerp  38447  ovnf  38448  hsphoidmvle2  38470  hsphoidmvle  38471  hoiprodp1  38473  hoidmv1lelem1  38476  hoidmv1lelem3  38478  hoidmv1le  38479  hoidmvlelem1  38480  hoidmvlelem2  38481  hoidmvlelem4  38483  ovnlecvr2  38495  hoidifhspdmvle  38505  hspmbllem1  38511  hspmbllem2  38512  hspmbllem3  38513  ovnovollem2  38542  2reu4  38702  issn  39088  uvtxa01vtx0  39571  rel1wlk  39741  cznrng  40282  lincolss  40552  lmodn0  40613  aacllem  40865