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

Theorem ssel2 3402
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)
Assertion
Ref Expression
ssel2  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )

Proof of Theorem ssel2
StepHypRef Expression
1 ssel 3401 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 430 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872    C_ wss 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3386  df-ss 3393
This theorem is referenced by:  tz7.7  5411  onfr  5424  onmindif  5474  ordunisssuc  5487  ssimaex  5890  nssdmovg  6409  onnmin  6588  onmindif2  6597  limsssuc  6635  1st2nd  6797  f1o2ndf1  6859  dfrecs3  7046  boxriin  7519  ordunifi  7774  isfinite2  7782  ordtypelem7  7992  sucprcreg  8067  cnfcom  8157  coflim  8642  cflim2  8644  fin23lem11  8698  fin23lem26  8706  fin1a2lem13  8793  fpwwe2lem12  9017  suplem2pr  9429  axpre-sup  9544  axsup  9660  dedekind  9748  dedekindle  9749  lbinf  10510  lbinfmOLD  10511  dfinfre  10539  dfinfmrOLD  10540  infmrclOLD  10544  infrelb  10547  infmrlbOLD  10548  suprfinzcl  11001  uzwo  11173  supminf  11201  supminfOLD  11202  lbzbi  11203  zsupss  11204  suprzcl2  11205  xrsupsslem  11543  xrinfmsslem  11544  xrub  11548  supxr2  11550  supxrun  11552  supxrunb1  11556  supxrbnd1  11558  supxrbnd2  11559  supxrub  11561  supxrbnd  11565  infxrlb  11571  infmxrlbOLD  11575  elfzom1elp1fzo  11931  ssfzo12  11954  fsuppmapnn0fiublem  12152  fsuppmapnn0fiub  12153  fsuppmapnn0fiub0  12155  seqsplit  12196  shftlem  13075  rpnnen2lem10  14219  rpnnen2lem11  14220  gcdcllem1  14416  mrcuni  15470  isacs1i  15506  mreacs  15507  lubss  16310  gsumwspan  16573  subgint  16784  cntziinsn  16931  cntzsubg  16933  pmtrdifellem4  17063  subrgint  17973  cntzsubr  17983  mdetunilem9  19587  tgcl  19927  fctop  19961  cctop  19963  neips  20071  cmpsub  20357  1stcelcls  20418  ssref  20469  comppfsc  20489  txbasval  20563  fgss2  20831  filcon  20840  filuni  20842  filssufilg  20868  fmfnfmlem4  20914  trust  21186  elmopn2  21402  metrest  21481  dscopn  21530  metds0  21809  metds0OLD  21824  cncfmet  21882  negcncf  21892  iscmet2  22206  ovolfioo  22362  ovolficc  22363  itg1mulc  22604  ply1term  23100  plyconst  23102  reeff1olem  23343  usgraedgrnv  25046  ghsubgolemOLD  26040  ocsh  26878  ocorth  26886  spansncvi  27247  pjss1coi  27758  sumdmdii  28010  dfcnv2  28225  xrge0infss  28290  xrge0infssOLD  28291  measres  28996  measdivcstOLD  28998  measdivcst  28999  dya2iocuni  29057  bnj1190  29769  frrlem5e  30473  nobndlem2  30531  nobndlem6  30535  nobndlem8  30537  nobndup  30538  nobnddown  30539  nofulllem3  30542  nofulllem4  30543  nofulllem5  30544  opnrebl  30925  opnrebl2  30926  fness  30954  fin2so  31839  poimirlem27  31874  poimir  31880  frinfm  31969  filbcmb  31974  nnubfi  31986  nninfnub  31987  sstotbnd3  32015  bndss  32025  exidreslem  32082  isidlc  32155  idlnegcl  32162  intidl  32169  unichnidl  32171  pmapglb2N  33248  elpaddn0  33277  paddasslem9  33305  paddasslem10  33306  pclfinN  33377  polval2N  33383  diaglbN  34535  dihord6apre  34736  snsslVD  37141  snssl  37142  sstrALT2VD  37146  sstrALT2  37147  suctrALTcf  37235  suctrALTcfVD  37236  ssnel  37282  uzwo4  37308  sge0iunmptlemfi  38106  caratheodorylem2  38199  ovnlerp  38231  ssfz12  38852  usgruspgrb  39033  uhgraedgrnv  39264  lindslinindimp2lem4  39857  lindslinindsimp2  39859  lincresunit3lem2  39876  lincresunit3  39877
  Copyright terms: Public domain W3C validator