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

Theorem ssel2 3345
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 3344 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 420 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  tz7.7  4610  onfr  4623  onmindif  4674  ordunisssuc  4687  onnmin  4786  onmindif2  4795  limsssuc  4833  ssimaex  5791  nssdmovg  6232  1st2nd  6396  f1o2ndf1  6457  boxriin  7107  ordunifi  7360  isfinite2  7368  ordtypelem7  7496  cnfcom  7660  coflim  8146  cflim2  8148  fin23lem11  8202  fin23lem26  8210  fin1a2lem13  8297  fpwwe2lem12  8521  suplem2pr  8935  axpre-sup  9049  axsup  9156  lbinfm  9966  dfinfmr  9990  infmrcl  9992  infmrlb  9994  uzwo  10544  uzwoOLD  10545  supminf  10568  lbzbi  10569  zsupss  10570  suprzcl2  10571  xrsupsslem  10890  xrinfmsslem  10891  xrub  10895  supxr2  10897  supxrun  10899  supxrunb1  10903  supxrbnd1  10905  supxrbnd2  10906  supxrub  10908  supxrbnd  10912  infmxrlb  10917  seqsplit  11361  shftlem  11888  rpnnen2lem10  12828  rpnnen2lem11  12829  gcdcllem1  13016  mrcuni  13851  isacs1i  13887  mreacs  13888  lubss  14553  gsumwspan  14796  subgint  14969  cntziinsn  15138  cntzsubg  15140  subrgint  15895  cntzsubr  15905  tgcl  17039  fctop  17073  cctop  17075  neips  17182  cmpsub  17468  1stcelcls  17529  txbasval  17643  fgss2  17911  filcon  17920  filuni  17922  filssufilg  17948  fmfnfmlem4  17994  trust  18264  elmopn2  18480  metrest  18559  dscopn  18626  metds0  18885  cncfmet  18943  negcncf  18953  iscmet2  19252  ovolfioo  19369  ovolficc  19370  itg1mulc  19599  ply1term  20128  plyconst  20130  reeff1olem  20367  usgraedgrnv  21402  ghsubgolem  21963  ocsh  22790  ocorth  22798  spansncvi  23159  pjss1coi  23671  sumdmdii  23923  measres  24581  measdivcstOLD  24583  measdivcst  24584  dya2iocuni  24638  dedekind  25192  dedekindle  25193  frrlem5e  25595  nobndlem2  25653  nobndlem6  25657  nobndlem8  25659  nobndup  25660  nobnddown  25661  nofulllem3  25664  nofulllem4  25665  nofulllem5  25666  opnrebl  26337  opnrebl2  26338  fness  26376  ssref  26377  comppfsc  26401  frinfm  26451  filbcmb  26456  nnubfi  26468  nninfnub  26469  sstotbnd3  26499  bndss  26509  exidreslem  26566  isidlc  26639  idlnegcl  26646  intidl  26653  unichnidl  26655  ssfz12  28127  ssfzo12  28153  lswrdcshw  28300  uhgraedgrnv  28326  snsslVD  29015  snssl  29016  sstrALT2VD  29020  sstrALT2  29021  suctrALTcf  29108  suctrALTcfVD  29109  bnj1190  29451  pmapglb2N  30642  elpaddn0  30671  paddasslem9  30699  paddasslem10  30700  pclfinN  30771  polval2N  30777  diaglbN  31927  dihord6apre  32128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator