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

Theorem ssel2 3481
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 3480 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 429 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1802    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  tz7.7  4890  onfr  4903  onmindif  4953  ordunisssuc  4966  ssimaex  5919  nssdmovg  6438  onnmin  6619  onmindif2  6628  limsssuc  6666  1st2nd  6827  f1o2ndf1  6889  boxriin  7509  ordunifi  7768  isfinite2  7776  ordtypelem7  7947  sucprcreg  8023  cnfcom  8142  cnfcomOLD  8150  coflim  8639  cflim2  8641  fin23lem11  8695  fin23lem26  8703  fin1a2lem13  8790  fpwwe2lem12  9017  suplem2pr  9429  axpre-sup  9544  axsup  9658  dedekind  9742  dedekindle  9743  lbinfm  10497  dfinfmr  10521  infmrcl  10523  infmrlb  10525  suprfinzcl  10978  uzwo  11148  uzwoOLD  11149  supminf  11173  lbzbi  11174  zsupss  11175  suprzcl2  11176  xrsupsslem  11502  xrinfmsslem  11503  xrub  11507  supxr2  11509  supxrun  11511  supxrunb1  11515  supxrbnd1  11517  supxrbnd2  11518  supxrub  11520  supxrbnd  11524  infmxrlb  11529  elfzom1elp1fzo  11857  ssfzo12  11879  fsuppmapnn0fiublem  12070  fsuppmapnn0fiub  12071  fsuppmapnn0fiub0  12073  seqsplit  12114  shftlem  12875  rpnnen2lem10  13829  rpnnen2lem11  13830  gcdcllem1  14021  mrcuni  14890  isacs1i  14926  mreacs  14927  lubss  15620  gsumwspan  15883  subgint  16094  cntziinsn  16241  cntzsubg  16243  pmtrdifellem4  16373  subrgint  17319  cntzsubr  17329  mdetunilem9  18989  tgcl  19337  fctop  19371  cctop  19373  neips  19480  cmpsub  19766  1stcelcls  19828  ssref  19879  comppfsc  19899  txbasval  19973  fgss2  20241  filcon  20250  filuni  20252  filssufilg  20278  fmfnfmlem4  20324  trust  20598  elmopn2  20814  metrest  20893  dscopn  20960  metds0  21220  cncfmet  21278  negcncf  21288  iscmet2  21599  ovolfioo  21745  ovolficc  21746  itg1mulc  21977  ply1term  22467  plyconst  22469  reeff1olem  22706  usgraedgrnv  24242  ghsubgolemOLD  25237  ocsh  26066  ocorth  26074  spansncvi  26435  pjss1coi  26947  sumdmdii  27199  dfcnv2  27382  xrge0infss  27445  measres  28059  measdivcstOLD  28061  measdivcst  28062  dya2iocuni  28120  frrlem5e  29363  nobndlem2  29421  nobndlem6  29425  nobndlem8  29427  nobndup  29428  nobnddown  29429  nofulllem3  29432  nofulllem4  29433  nofulllem5  29434  fin2so  30008  opnrebl  30106  opnrebl2  30107  fness  30135  frinfm  30194  filbcmb  30199  nnubfi  30211  nninfnub  30212  sstotbnd3  30240  bndss  30250  exidreslem  30307  isidlc  30380  idlnegcl  30387  intidl  30394  unichnidl  30396  ssnel  31370  ssfz12  32164  uhgraedgrnv  32183  lindslinindimp2lem4  32772  lindslinindsimp2  32774  lincresunit3lem2  32791  lincresunit3  32792  snsslVD  33337  snssl  33338  sstrALT2VD  33342  sstrALT2  33343  suctrALTcf  33430  suctrALTcfVD  33431  bnj1190  33771  pmapglb2N  35197  elpaddn0  35226  paddasslem9  35254  paddasslem10  35255  pclfinN  35326  polval2N  35332  diaglbN  36484  dihord6apre  36685
  Copyright terms: Public domain W3C validator