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

Theorem ne0i 3626
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 3625 . 2  |-  ( B  e.  A  ->  -.  A  =  (/) )
21neneqad 2668 1  |-  ( B  e.  A  ->  A  =/=  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725    =/= wne 2598   (/)c0 3620
This theorem is referenced by:  vn0  3627  inelcm  3674  rzal  3721  rexn0  3722  snnzg  3913  prnz  3915  tpnz  3917  exss  4418  ord0eln0  4627  onn0  4637  fr3nr  4752  onnmin  4775  elfvdm  5749  isofrlem  6052  f1oweALT  6066  bropopvvv  6418  frxp  6448  mpt2xopxnop0  6458  brovex  6466  onnseq  6598  oe1m  6780  oawordeulem  6789  oa00  6794  oarec  6797  omord  6803  oewordri  6827  oeordsuc  6829  oelim2  6830  oeoalem  6831  oeoelem  6833  oeeui  6837  nnmord  6867  nnawordex  6872  map0g  7045  ixpn0  7086  omxpenlem  7201  frfi  7344  unblem1  7351  wofib  7506  canthwdom  7539  inf1  7569  noinfep  7606  noinfepOLD  7607  oemapvali  7632  cantnflem1a  7633  cantnflem1d  7636  cantnflem1  7637  cantnf  7641  epfrs  7659  acnrcl  7915  iunfictbso  7987  dfac5lem2  7997  dfac9  8008  kmlem6  8027  fin23lem31  8215  fin23lem40  8223  isf34lem7  8251  isf34lem6  8252  isfin1-3  8258  fin1a2lem7  8278  fin1a2lem13  8284  axdc3lem4  8325  alephval2  8439  omina  8558  intwun  8602  r1limwun  8603  tskpr  8637  inar1  8642  tskuni  8650  tskxp  8654  tskmap  8655  gruina  8685  grur1a  8686  grur1  8687  axgroth3  8698  inaprc  8703  addclpi  8761  mulclpi  8762  indpi  8776  nqerf  8799  genpn0  8872  supsrlem  8978  axpre-sup  9036  infmrcl  9979  infmrlb  9981  uzn0  10493  infmssuzle  10550  suprzub  10559  rpnnen1lem4  10595  rpnnen1lem5  10596  eliooxr  10961  iccssioo2  10975  iccsupr  10989  fzn0  11062  elfzoel1  11130  elfzoel2  11131  fzon0  11148  flval3  11214  icopnfsup  11238  fseqsupubi  11309  hashnn0n0nn  11656  sqrlem3  12042  rexfiuz  12143  r19.2uz  12147  climuni  12338  isercolllem2  12451  isercolllem3  12452  climsup  12455  caurcvg  12462  caurcvg2  12463  caucvg  12464  infcvgaux1i  12628  mertenslem2  12654  ruclem11  12831  divalglem2  12907  gcdcllem1  13003  bezoutlem2  13031  pclem  13204  pc2dvds  13244  prmreclem1  13276  prmreclem6  13281  4sqlem13  13317  vdwmc2  13339  vdwlem6  13346  vdwlem8  13348  vdwnnlem3  13357  ramtcl  13370  mrcflem  13823  mrcval  13827  iscatd2  13898  fpwipodrs  14582  gsumval2  14775  grpbn0  14826  issubg3  14952  issubg4  14953  subgint  14956  cycsubgcl  14958  nmzsubg  14973  ghmpreima  15019  brgici  15049  gastacl  15078  odlem2  15169  gexlem2  15208  sylow1lem5  15228  pgpssslw  15240  sylow2alem2  15244  sylow2blem3  15248  fislw  15251  sylow3lem3  15255  sylow3lem4  15256  torsubg  15461  oddvdssubg  15462  iscygd  15489  iscygodd  15490  cyggexb  15500  gsumval3  15506  dprdsubg  15574  ablfacrp2  15617  ablfac1c  15621  ablfac1eu  15623  pgpfaclem2  15632  subrgugrp  15879  cntzsubr  15892  islss4  16030  lss1d  16031  lssintcl  16032  brlmici  16133  lspsolvlem  16206  lbsextlem1  16222  issubgrpd2  16252  lidlsubg  16278  abvn0b  16354  psrbas  16435  mplsubglem  16490  mpllsslem  16491  ltbwe  16525  mplind  16554  ply1plusgfvi  16628  cnsubglem  16739  cnmsubglem  16753  zlpirlem1  16760  ocvlss  16891  clscld  17103  clsval2  17106  lmmo  17436  1stcfb  17500  2ndcdisj  17511  2ndcsep  17514  ptclsg  17639  dfac14lem  17641  txindis  17658  hmphi  17801  opnfbas  17866  trfbas2  17867  isfil2  17880  filn0  17886  zfbas  17920  filssufilg  17935  rnelfmlem  17976  flimclslem  18008  flimfnfcls  18052  ptcmplem2  18076  clssubg  18130  tgpconcomp  18134  tsmsfbas  18149  ustfilxp  18234  ustne0  18235  prdsmet  18392  xbln0  18436  bln0  18437  prdsbl  18513  metustfbasOLD  18587  metustfbas  18588  metustblOLD  18602  metustbl  18603  nrgdomn  18699  nrginvrcn  18719  tgioo  18819  icccmplem2  18846  icccmplem3  18847  reconnlem2  18850  lebnumlem3  18980  phtpcer  19012  reparpht  19015  phtpcco2  19016  pcohtpy  19037  pcorevlem  19043  caun0  19226  iscmet3lem2  19237  bcthlem4  19272  cnflduss  19302  cnfldcusp  19303  minveclem3b  19321  ivthlem2  19341  ivthlem3  19342  evthicc  19348  ovollb2  19377  ovolctb  19378  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliun2  19394  nulmbl2  19423  ioombl1lem4  19447  uniioombllem1  19465  uniioombllem2  19467  uniioombllem6  19472  mbfsup  19548  mbfinf  19549  mbflimsup  19550  itg1climres  19598  itg2seq  19626  itg2monolem1  19634  itg2mono  19637  itg2i1fseq2  19640  dvferm1lem  19860  dvferm2lem  19862  dvferm  19864  c1liplem1  19872  c1lip1  19873  dvivthlem1  19884  mpfrcl  19931  aannenlem2  20238  aalioulem2  20242  ulm0  20299  pilem2  20360  pilem3  20361  birthdaylem1  20782  ftalem3  20849  ftalem4  20850  ftalem5  20851  dchrabs  21036  pntlem3  21295  ghgrp  21948  nvo00  22254  nmorepnf  22261  ubthlem1  22364  minvecolem1  22368  shintcl  22824  chintcl  22826  nmoprepnf  23362  nmfnrepnf  23375  nmcexi  23521  snct  24095  rge0scvg  24327  reust  24336  recusp  24337  qqhucn  24368  rrhre  24379  esum0  24436  esumpcvgval  24460  sigagenval  24515  voliune  24577  erdszelem2  24870  erdszelem8  24876  txsconlem  24919  cvxscon  24922  cvmsss2  24953  cvmliftmolem2  24961  cvmlift2lem12  24993  cvmliftpht  24997  dfrtrcl2  25140  dfso3  25169  sltval2  25603  nocvxminlem  25637  nobndlem5  25643  axlowdimlem13  25885  axlowdim1  25890  onint1  26191  mblfinlem  26234  ismblfin  26237  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  itg2addnclem  26246  itg2addnc  26249  ftc1anclem7  26276  ftc1anc  26278  finminlem  26312  fnemeet1  26386  fnejoin1  26388  tailfb  26397  incsequz  26443  isbnd3  26484  ssbnd  26488  totbndbnd  26489  prdsbnd  26493  prdsbnd2  26495  heibor1lem  26509  prtlem100  26695  prter3  26722  nacsfix  26757  mzpcln0  26776  rencldnfilem  26872  rencldnfi  26873  fnwe2lem2  27117  kelac1  27129  harn0  27235  lmiclbs  27275  lmisfree  27280  hbtlem2  27296  rzalf  27655  ubelsupr  27658  climinf  27699  stoweidlem11  27727  stoweidlem31  27747  stoweidlem34  27750  stoweidlem36  27752  stoweidlem59  27775  stirlinglem13  27802  2reu4  27935  2wlkonot3v  28295  2spthonot3v  28296  usg2spthonot  28308  usg2spthonot0  28309  2spot2iun2spont  28311  frg2wotn0  28382  bnj906  29238  bnj1177  29312  bnj1523  29377  lkrlss  29830  ishlat3N  30089  hlsupr2  30121  elpaddri  30536  pclvalN  30624  dian0  31774  diaintclN  31793  docaclN  31859  dibintclN  31902  dicn0  31927  dihglblem5  32033  dihglb2  32077  dihintcl  32079  doch2val2  32099  dochocss  32101  lclkr  32268  lclkrs  32274  lcfr  32320
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator