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

Theorem ne0i 3474
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 3473 . 2  |-  ( B  e.  A  ->  -.  A  =  (/) )
2 df-ne 2461 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
31, 2sylibr 203 1  |-  ( B  e.  A  ->  A  =/=  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    e. wcel 1696    =/= wne 2459   (/)c0 3468
This theorem is referenced by:  vn0  3475  inelcm  3522  rzal  3568  rexn0  3569  snnzg  3756  prnz  3758  tpnz  3760  exss  4252  ord0eln0  4462  onn0  4472  fr3nr  4587  onnmin  4610  elfvdm  5570  isofrlem  5853  f1oweALT  5867  frxp  6241  onnseq  6377  oe1m  6559  oawordeulem  6568  oa00  6573  oarec  6576  omord  6582  oewordri  6606  oeordsuc  6608  oelim2  6609  oeoalem  6610  oeoelem  6612  oeeui  6616  nnmord  6646  nnawordex  6651  map0g  6823  ixpn0  6864  omxpenlem  6979  frfi  7118  unblem1  7125  wofib  7276  canthwdom  7309  inf1  7339  noinfep  7376  noinfepOLD  7377  oemapvali  7402  cantnflem1a  7403  cantnflem1d  7406  cantnflem1  7407  cantnf  7411  epfrs  7429  acnrcl  7685  iunfictbso  7757  dfac5lem2  7767  dfac9  7778  kmlem6  7797  fin23lem31  7985  fin23lem40  7993  isf34lem7  8021  isf34lem6  8022  isfin1-3  8028  fin1a2lem7  8048  fin1a2lem13  8054  axdc3lem4  8095  alephval2  8210  omina  8329  intwun  8373  r1limwun  8374  tskpr  8408  inar1  8413  tskuni  8421  tskxp  8425  tskmap  8426  gruina  8456  grur1a  8457  grur1  8458  axgroth3  8469  inaprc  8474  addclpi  8532  mulclpi  8533  indpi  8547  nqerf  8570  genpn0  8643  supsrlem  8749  axpre-sup  8807  infmrcl  9749  infmrlb  9751  uzn0  10259  infmssuzle  10316  suprzub  10325  rpnnen1lem4  10361  rpnnen1lem5  10362  eliooxr  10725  iccssioo2  10738  iccsupr  10752  fzn0  10825  elfzoel1  10889  elfzoel2  10890  fzon0  10907  flval3  10961  icopnfsup  10985  fseqsupubi  11056  sqrlem3  11746  rexfiuz  11847  r19.2uz  11851  climuni  12042  isercolllem2  12155  isercolllem3  12156  climsup  12159  caurcvg  12165  caurcvg2  12166  caucvg  12167  infcvgaux1i  12331  mertenslem2  12357  ruclem11  12534  divalglem2  12610  gcdcllem1  12706  bezoutlem2  12734  pclem  12907  pc2dvds  12947  prmreclem1  12979  prmreclem6  12984  4sqlem13  13020  vdwmc2  13042  vdwlem6  13049  vdwlem8  13051  vdwnnlem3  13060  ramtcl  13073  mrcflem  13524  mrcval  13528  iscatd2  13599  fpwipodrs  14283  gsumval2  14476  grpbn0  14527  issubg3  14653  issubg4  14654  subgint  14657  cycsubgcl  14659  nmzsubg  14674  ghmpreima  14720  brgici  14750  gastacl  14779  odlem2  14870  gexlem2  14909  sylow1lem5  14929  pgpssslw  14941  sylow2alem2  14945  sylow2blem3  14949  fislw  14952  sylow3lem3  14956  sylow3lem4  14957  torsubg  15162  oddvdssubg  15163  iscygd  15190  iscygodd  15191  cyggexb  15201  gsumval3  15207  dprdsubg  15275  ablfacrp2  15318  ablfac1c  15322  ablfac1eu  15324  pgpfaclem2  15333  subrgugrp  15580  cntzsubr  15593  islss4  15735  lss1d  15736  lssintcl  15737  brlmici  15838  lspsolvlem  15911  lbsextlem1  15927  issubgrpd2  15957  lidlsubg  15983  abvn0b  16059  psrbas  16140  mplsubglem  16195  mpllsslem  16196  ltbwe  16230  mplind  16259  ply1plusgfvi  16336  cnsubglem  16436  cnmsubglem  16450  zlpirlem1  16457  ocvlss  16588  clscld  16800  clsval2  16803  lmmo  17124  1stcfb  17187  2ndcdisj  17198  2ndcsep  17201  ptclsg  17325  dfac14lem  17327  txindis  17344  hmphi  17484  opnfbas  17553  trfbas2  17554  isfil2  17567  filn0  17573  zfbas  17607  filssufilg  17622  rnelfmlem  17663  flimclslem  17695  flimfnfcls  17739  ptcmplem2  17763  clssubg  17807  tgpconcomp  17811  tsmsfbas  17826  prdsmet  17950  xbln0  17981  bln0  17982  prdsbl  18053  nrgdomn  18198  nrginvrcn  18218  tgioo  18318  icccmplem2  18344  icccmplem3  18345  reconnlem2  18348  lebnumlem3  18477  phtpcer  18509  reparpht  18512  phtpcco2  18513  pcohtpy  18534  pcorevlem  18540  caun0  18723  iscmet3lem2  18734  bcthlem4  18765  minveclem3b  18808  ivthlem2  18828  ivthlem3  18829  evthicc  18835  ovollb2  18864  ovolctb  18865  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliun2  18881  nulmbl2  18910  ioombl1lem4  18934  uniioombllem1  18952  uniioombllem2  18954  uniioombllem6  18959  mbfsup  19035  mbfinf  19036  mbflimsup  19037  itg1climres  19085  itg2seq  19113  itg2monolem1  19121  itg2mono  19124  itg2i1fseq2  19127  dvferm1lem  19347  dvferm2lem  19349  dvferm  19351  c1liplem1  19359  c1lip1  19360  dvivthlem1  19371  mpfrcl  19418  aannenlem2  19725  aalioulem2  19729  ulm0  19786  pilem2  19844  pilem3  19845  birthdaylem1  20262  ftalem3  20328  ftalem4  20329  ftalem5  20330  dchrabs  20515  pntlem3  20774  ghgrp  21051  nvo00  21355  nmorepnf  21362  ubthlem1  21465  minvecolem1  21469  shintcl  21925  chintcl  21927  nmoprepnf  22463  nmfnrepnf  22476  nmcexi  22622  snct  23354  rge0scvg  23388  esum0  23443  esumpcvgval  23461  sigagenval  23516  indf1ofs  23624  erdszelem2  23738  erdszelem8  23744  txsconlem  23786  cvxscon  23789  cvmsss2  23820  cvmliftmolem2  23828  cvmlift2lem12  23860  cvmliftpht  23864  dfrtrcl2  24060  dfso3  24089  sltval2  24381  nocvxminlem  24415  nobndlem5  24421  axlowdimlem13  24654  axlowdim1  24659  onint1  24960  ovoliunnfl  25001  limhun  25673  hine  25900  tartarmap  25991  isconcl7a  26208  nbssntrs  26250  finminlem  26334  fnemeet1  26418  fnejoin1  26420  tailfb  26429  incsequz  26561  isbnd3  26611  ssbnd  26615  totbndbnd  26616  prdsbnd  26620  prdsbnd2  26622  heibor1lem  26636  prtlem100  26824  prter3  26853  nacsfix  26890  mzpcln0  26909  rencldnfilem  27006  rencldnfi  27007  fnwe2lem2  27251  kelac1  27264  harn0  27370  lmiclbs  27410  lmisfree  27415  hbtlem2  27431  rzalf  27791  ubelsupr  27794  climinf  27835  stoweidlem11  27863  stoweidlem31  27883  stoweidlem34  27886  stoweidlem36  27888  stoweidlem59  27911  stirlinglem13  27938  2reu4  28071  mpt2xopxnop0  28197  brovex  28205  trlonprop  28341  bnj906  29278  bnj1177  29352  bnj1523  29417  lkrlss  29907  ishlat3N  30166  hlsupr2  30198  elpaddri  30613  pclvalN  30701  dian0  31851  diaintclN  31870  docaclN  31936  dibintclN  31979  dicn0  32004  dihglblem5  32110  dihglb2  32154  dihintcl  32156  doch2val2  32176  dochocss  32178  lclkr  32345  lclkrs  32351  lcfr  32397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator