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

Theorem ne0i 3461
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 3460 . 2  |-  ( B  e.  A  ->  -.  A  =  (/) )
2 df-ne 2448 . 2  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
31, 2sylibr 203 1  |-  ( B  e.  A  ->  A  =/=  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    e. wcel 1684    =/= wne 2446   (/)c0 3455
This theorem is referenced by:  vn0  3462  inelcm  3509  rzal  3555  rexn0  3556  snnzg  3743  prnz  3745  tpnz  3747  exss  4236  ord0eln0  4446  onn0  4456  fr3nr  4571  onnmin  4594  elfvdm  5554  isofrlem  5837  f1oweALT  5851  frxp  6225  onnseq  6361  oe1m  6543  oawordeulem  6552  oa00  6557  oarec  6560  omord  6566  oewordri  6590  oeordsuc  6592  oelim2  6593  oeoalem  6594  oeoelem  6596  oeeui  6600  nnmord  6630  nnawordex  6635  map0g  6807  ixpn0  6848  omxpenlem  6963  frfi  7102  unblem1  7109  wofib  7260  canthwdom  7293  inf1  7323  noinfep  7360  noinfepOLD  7361  oemapvali  7386  cantnflem1a  7387  cantnflem1d  7390  cantnflem1  7391  cantnf  7395  epfrs  7413  acnrcl  7669  iunfictbso  7741  dfac5lem2  7751  dfac9  7762  kmlem6  7781  fin23lem31  7969  fin23lem40  7977  isf34lem7  8005  isf34lem6  8006  isfin1-3  8012  fin1a2lem7  8032  fin1a2lem13  8038  axdc3lem4  8079  alephval2  8194  omina  8313  intwun  8357  r1limwun  8358  tskpr  8392  inar1  8397  tskuni  8405  tskxp  8409  tskmap  8410  gruina  8440  grur1a  8441  grur1  8442  axgroth3  8453  inaprc  8458  addclpi  8516  mulclpi  8517  indpi  8531  nqerf  8554  genpn0  8627  supsrlem  8733  axpre-sup  8791  infmrcl  9733  infmrlb  9735  uzn0  10243  infmssuzle  10300  suprzub  10309  rpnnen1lem4  10345  rpnnen1lem5  10346  eliooxr  10709  iccssioo2  10722  iccsupr  10736  fzn0  10809  elfzoel1  10873  elfzoel2  10874  fzon0  10891  flval3  10945  icopnfsup  10969  fseqsupubi  11040  sqrlem3  11730  rexfiuz  11831  r19.2uz  11835  climuni  12026  isercolllem2  12139  isercolllem3  12140  climsup  12143  caurcvg  12149  caurcvg2  12150  caucvg  12151  infcvgaux1i  12315  mertenslem2  12341  ruclem11  12518  divalglem2  12594  gcdcllem1  12690  bezoutlem2  12718  pclem  12891  pc2dvds  12931  prmreclem1  12963  prmreclem6  12968  4sqlem13  13004  vdwmc2  13026  vdwlem6  13033  vdwlem8  13035  vdwnnlem3  13044  ramtcl  13057  mrcflem  13508  mrcval  13512  iscatd2  13583  fpwipodrs  14267  gsumval2  14460  grpbn0  14511  issubg3  14637  issubg4  14638  subgint  14641  cycsubgcl  14643  nmzsubg  14658  ghmpreima  14704  brgici  14734  gastacl  14763  odlem2  14854  gexlem2  14893  sylow1lem5  14913  pgpssslw  14925  sylow2alem2  14929  sylow2blem3  14933  fislw  14936  sylow3lem3  14940  sylow3lem4  14941  torsubg  15146  oddvdssubg  15147  iscygd  15174  iscygodd  15175  cyggexb  15185  gsumval3  15191  dprdsubg  15259  ablfacrp2  15302  ablfac1c  15306  ablfac1eu  15308  pgpfaclem2  15317  subrgugrp  15564  cntzsubr  15577  islss4  15719  lss1d  15720  lssintcl  15721  brlmici  15822  lspsolvlem  15895  lbsextlem1  15911  issubgrpd2  15941  lidlsubg  15967  abvn0b  16043  psrbas  16124  mplsubglem  16179  mpllsslem  16180  ltbwe  16214  mplind  16243  ply1plusgfvi  16320  cnsubglem  16420  cnmsubglem  16434  zlpirlem1  16441  ocvlss  16572  clscld  16784  clsval2  16787  lmmo  17108  1stcfb  17171  2ndcdisj  17182  2ndcsep  17185  ptclsg  17309  dfac14lem  17311  txindis  17328  hmphi  17468  opnfbas  17537  trfbas2  17538  isfil2  17551  filn0  17557  zfbas  17591  filssufilg  17606  rnelfmlem  17647  flimclslem  17679  flimfnfcls  17723  ptcmplem2  17747  clssubg  17791  tgpconcomp  17795  tsmsfbas  17810  prdsmet  17934  xbln0  17965  bln0  17966  prdsbl  18037  nrgdomn  18182  nrginvrcn  18202  tgioo  18302  icccmplem2  18328  icccmplem3  18329  reconnlem2  18332  lebnumlem3  18461  phtpcer  18493  reparpht  18496  phtpcco2  18497  pcohtpy  18518  pcorevlem  18524  caun0  18707  iscmet3lem2  18718  bcthlem4  18749  minveclem3b  18792  ivthlem2  18812  ivthlem3  18813  evthicc  18819  ovollb2  18848  ovolctb  18849  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliun2  18865  nulmbl2  18894  ioombl1lem4  18918  uniioombllem1  18936  uniioombllem2  18938  uniioombllem6  18943  mbfsup  19019  mbfinf  19020  mbflimsup  19021  itg1climres  19069  itg2seq  19097  itg2monolem1  19105  itg2mono  19108  itg2i1fseq2  19111  dvferm1lem  19331  dvferm2lem  19333  dvferm  19335  c1liplem1  19343  c1lip1  19344  dvivthlem1  19355  mpfrcl  19402  aannenlem2  19709  aalioulem2  19713  ulm0  19770  pilem2  19828  pilem3  19829  birthdaylem1  20246  ftalem3  20312  ftalem4  20313  ftalem5  20314  dchrabs  20499  pntlem3  20758  ghgrp  21035  nvo00  21339  nmorepnf  21346  ubthlem1  21449  minvecolem1  21453  shintcl  21909  chintcl  21911  nmoprepnf  22447  nmfnrepnf  22460  nmcexi  22606  snct  23339  rge0scvg  23373  esum0  23428  esumpcvgval  23446  sigagenval  23501  indf1ofs  23609  erdszelem2  23723  erdszelem8  23729  txsconlem  23771  cvxscon  23774  cvmsss2  23805  cvmliftmolem2  23813  cvmlift2lem12  23845  cvmliftpht  23849  dfrtrcl2  24045  dfso3  24074  sltval2  24310  nocvxminlem  24344  nobndlem5  24350  axlowdimlem13  24582  axlowdim1  24587  onint1  24888  limhun  25570  hine  25797  tartarmap  25888  isconcl7a  26105  nbssntrs  26147  finminlem  26231  fnemeet1  26315  fnejoin1  26317  tailfb  26326  incsequz  26458  isbnd3  26508  ssbnd  26512  totbndbnd  26513  prdsbnd  26517  prdsbnd2  26519  heibor1lem  26533  prtlem100  26721  prter3  26750  nacsfix  26787  mzpcln0  26806  rencldnfilem  26903  rencldnfi  26904  fnwe2lem2  27148  kelac1  27161  harn0  27267  lmiclbs  27307  lmisfree  27312  hbtlem2  27328  rzalf  27688  ubelsupr  27691  climinf  27732  stoweidlem11  27760  stoweidlem31  27780  stoweidlem34  27783  stoweidlem36  27785  stoweidlem59  27808  stirlinglem13  27835  2reu4  27968  mpt2xopxnop0  28081  bnj906  28962  bnj1177  29036  bnj1523  29101  lkrlss  29285  ishlat3N  29544  hlsupr2  29576  elpaddri  29991  pclvalN  30079  dian0  31229  diaintclN  31248  docaclN  31314  dibintclN  31357  dicn0  31382  dihglblem5  31488  dihglb2  31532  dihintcl  31534  doch2val2  31554  dochocss  31556  lclkr  31723  lclkrs  31729  lcfr  31775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator