MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ne0i Structured version   Unicode version

Theorem ne0i 3636
Description: If a set has elements, it is not empty. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
ne0i  |-  ( B  e.  A  ->  A  =/=  (/) )

Proof of Theorem ne0i
StepHypRef Expression
1 n0i 3635 . 2  |-  ( B  e.  A  ->  -.  A  =  (/) )
21neneqad 2676 1  |-  ( B  e.  A  ->  A  =/=  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    =/= wne 2601   (/)c0 3630
This theorem is referenced by:  vn0  3637  inelcm  3684  rzal  3731  rexn0  3732  snnzg  3923  prnz  3925  tpnz  3927  exss  4429  ord0eln0  4638  onn0  4648  fr3nr  4763  onnmin  4786  elfvdm  5760  isofrlem  6063  f1oweALT  6077  bropopvvv  6429  frxp  6459  mpt2xopxnop0  6469  brovex  6477  onnseq  6609  oe1m  6791  oawordeulem  6800  oa00  6805  oarec  6808  omord  6814  oewordri  6838  oeordsuc  6840  oelim2  6841  oeoalem  6842  oeoelem  6844  oeeui  6848  nnmord  6878  nnawordex  6883  map0g  7056  ixpn0  7097  omxpenlem  7212  frfi  7355  unblem1  7362  wofib  7517  canthwdom  7550  inf1  7580  noinfep  7617  noinfepOLD  7618  oemapvali  7643  cantnflem1a  7644  cantnflem1d  7647  cantnflem1  7648  cantnf  7652  epfrs  7670  acnrcl  7928  iunfictbso  8000  dfac5lem2  8010  dfac9  8021  kmlem6  8040  fin23lem31  8228  fin23lem40  8236  isf34lem7  8264  isf34lem6  8265  isfin1-3  8271  fin1a2lem7  8291  fin1a2lem13  8297  axdc3lem4  8338  alephval2  8452  omina  8571  intwun  8615  r1limwun  8616  tskpr  8650  inar1  8655  tskuni  8663  tskxp  8667  tskmap  8668  gruina  8698  grur1a  8699  grur1  8700  axgroth3  8711  inaprc  8716  addclpi  8774  mulclpi  8775  indpi  8789  nqerf  8812  genpn0  8885  supsrlem  8991  axpre-sup  9049  infmrcl  9992  infmrlb  9994  uzn0  10506  infmssuzle  10563  suprzub  10572  rpnnen1lem4  10608  rpnnen1lem5  10609  eliooxr  10974  iccssioo2  10988  iccsupr  11002  fzn0  11075  elfzoel1  11143  elfzoel2  11144  fzon0  11161  flval3  11227  icopnfsup  11251  fseqsupubi  11322  hashnn0n0nn  11669  sqrlem3  12055  rexfiuz  12156  r19.2uz  12160  climuni  12351  isercolllem2  12464  isercolllem3  12465  climsup  12468  caurcvg  12475  caurcvg2  12476  caucvg  12477  infcvgaux1i  12641  mertenslem2  12667  ruclem11  12844  divalglem2  12920  gcdcllem1  13016  bezoutlem2  13044  pclem  13217  pc2dvds  13257  prmreclem1  13289  prmreclem6  13294  4sqlem13  13330  vdwmc2  13352  vdwlem6  13359  vdwlem8  13361  vdwnnlem3  13370  ramtcl  13383  mrcflem  13836  mrcval  13840  iscatd2  13911  fpwipodrs  14595  gsumval2  14788  grpbn0  14839  issubg3  14965  issubg4  14966  subgint  14969  cycsubgcl  14971  nmzsubg  14986  ghmpreima  15032  brgici  15062  gastacl  15091  odlem2  15182  gexlem2  15221  sylow1lem5  15241  pgpssslw  15253  sylow2alem2  15257  sylow2blem3  15261  fislw  15264  sylow3lem3  15268  sylow3lem4  15269  torsubg  15474  oddvdssubg  15475  iscygd  15502  iscygodd  15503  cyggexb  15513  gsumval3  15519  dprdsubg  15587  ablfacrp2  15630  ablfac1c  15634  ablfac1eu  15636  pgpfaclem2  15645  subrgugrp  15892  cntzsubr  15905  islss4  16043  lss1d  16044  lssintcl  16045  brlmici  16146  lspsolvlem  16219  lbsextlem1  16235  issubgrpd2  16265  lidlsubg  16291  abvn0b  16367  psrbas  16448  mplsubglem  16503  mpllsslem  16504  ltbwe  16538  mplind  16567  ply1plusgfvi  16641  cnsubglem  16752  cnmsubglem  16766  zlpirlem1  16773  ocvlss  16904  clscld  17116  clsval2  17119  lmmo  17449  1stcfb  17513  2ndcdisj  17524  2ndcsep  17527  ptclsg  17652  dfac14lem  17654  txindis  17671  hmphi  17814  opnfbas  17879  trfbas2  17880  isfil2  17893  filn0  17899  zfbas  17933  filssufilg  17948  rnelfmlem  17989  flimclslem  18021  flimfnfcls  18065  ptcmplem2  18089  clssubg  18143  tgpconcomp  18147  tsmsfbas  18162  ustfilxp  18247  ustne0  18248  prdsmet  18405  xbln0  18449  bln0  18450  prdsbl  18526  metustfbasOLD  18600  metustfbas  18601  metustblOLD  18615  metustbl  18616  nrgdomn  18712  nrginvrcn  18732  tgioo  18832  icccmplem2  18859  icccmplem3  18860  reconnlem2  18863  lebnumlem3  18993  phtpcer  19025  reparpht  19028  phtpcco2  19029  pcohtpy  19050  pcorevlem  19056  caun0  19239  iscmet3lem2  19250  bcthlem4  19285  cnflduss  19315  cnfldcusp  19316  minveclem3b  19334  ivthlem2  19354  ivthlem3  19355  evthicc  19361  ovollb2  19390  ovolctb  19391  ovolunlem1a  19397  ovolunlem1  19398  ovoliunlem1  19403  ovoliun2  19407  nulmbl2  19436  ioombl1lem4  19460  uniioombllem1  19478  uniioombllem2  19480  uniioombllem6  19485  mbfsup  19559  mbfinf  19560  mbflimsup  19561  itg1climres  19609  itg2seq  19637  itg2monolem1  19645  itg2mono  19648  itg2i1fseq2  19651  dvferm1lem  19873  dvferm2lem  19875  dvferm  19877  c1liplem1  19885  c1lip1  19886  dvivthlem1  19897  mpfrcl  19944  aannenlem2  20251  aalioulem2  20255  ulm0  20312  pilem2  20373  pilem3  20374  birthdaylem1  20795  ftalem3  20862  ftalem4  20863  ftalem5  20864  dchrabs  21049  pntlem3  21308  ghgrp  21961  nvo00  22267  nmorepnf  22274  ubthlem1  22377  minvecolem1  22381  shintcl  22837  chintcl  22839  nmoprepnf  23375  nmfnrepnf  23388  nmcexi  23534  snct  24108  rge0scvg  24340  reust  24349  recusp  24350  qqhucn  24381  rrhre  24392  esum0  24449  esumpcvgval  24473  sigagenval  24528  voliune  24590  erdszelem2  24883  erdszelem8  24889  txsconlem  24932  cvxscon  24935  cvmsss2  24966  cvmliftmolem2  24974  cvmlift2lem12  25006  cvmliftpht  25010  dfrtrcl2  25153  dfso3  25182  sltval2  25616  nocvxminlem  25650  nobndlem5  25656  axlowdimlem13  25898  axlowdim1  25903  onint1  26204  heicant  26253  mblfinlem2  26256  ismblfin  26259  ovoliunnfl  26260  voliunnfl  26262  volsupnfl  26263  itg2addnclem  26270  itg2addnc  26273  ftc1anclem7  26300  ftc1anc  26302  finminlem  26335  fnemeet1  26409  fnejoin1  26411  tailfb  26420  incsequz  26466  isbnd3  26507  ssbnd  26511  totbndbnd  26512  prdsbnd  26516  prdsbnd2  26518  heibor1lem  26532  prtlem100  26718  prter3  26745  nacsfix  26780  mzpcln0  26799  rencldnfilem  26895  rencldnfi  26896  fnwe2lem2  27140  kelac1  27152  harn0  27258  lmiclbs  27298  lmisfree  27303  hbtlem2  27319  rzalf  27678  ubelsupr  27681  climinf  27722  stoweidlem11  27750  stoweidlem31  27770  stoweidlem34  27773  stoweidlem36  27775  stoweidlem59  27798  stirlinglem13  27825  2reu4  27958  breqn0  28084  elovmpt3rab1  28107  2wlkonot3v  28407  2spthonot3v  28408  usg2spthonot  28420  usg2spthonot0  28421  2spot2iun2spont  28423  frg2wotn0  28519  bnj906  29375  bnj1177  29449  bnj1523  29514  lkrlss  29967  ishlat3N  30226  hlsupr2  30258  elpaddri  30673  pclvalN  30761  dian0  31911  diaintclN  31930  docaclN  31996  dibintclN  32039  dicn0  32064  dihglblem5  32170  dihglb2  32214  dihintcl  32216  doch2val2  32236  dochocss  32238  lclkr  32405  lclkrs  32411  lcfr  32457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-nul 3631
  Copyright terms: Public domain W3C validator