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

Theorem ssel2 3335
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 3334 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 419 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725    C_ wss 3312
This theorem is referenced by:  tz7.7  4599  onfr  4612  onmindif  4663  ordunisssuc  4676  onnmin  4775  onmindif2  4784  limsssuc  4822  ssimaex  5780  nssdmovg  6221  1st2nd  6385  f1o2ndf1  6446  boxriin  7096  ordunifi  7349  isfinite2  7357  ordtypelem7  7485  cnfcom  7649  coflim  8133  cflim2  8135  fin23lem11  8189  fin23lem26  8197  fin1a2lem13  8284  fpwwe2lem12  8508  suplem2pr  8922  axpre-sup  9036  axsup  9143  lbinfm  9953  dfinfmr  9977  infmrcl  9979  infmrlb  9981  uzwo  10531  uzwoOLD  10532  supminf  10555  lbzbi  10556  zsupss  10557  suprzcl2  10558  xrsupsslem  10877  xrinfmsslem  10878  xrub  10882  supxr2  10884  supxrun  10886  supxrunb1  10890  supxrbnd1  10892  supxrbnd2  10893  supxrub  10895  supxrbnd  10899  infmxrlb  10904  seqsplit  11348  shftlem  11875  rpnnen2lem10  12815  rpnnen2lem11  12816  gcdcllem1  13003  mrcuni  13838  isacs1i  13874  mreacs  13875  lubss  14540  gsumwspan  14783  subgint  14956  cntziinsn  15125  cntzsubg  15127  subrgint  15882  cntzsubr  15892  tgcl  17026  fctop  17060  cctop  17062  neips  17169  cmpsub  17455  1stcelcls  17516  txbasval  17630  fgss2  17898  filcon  17907  filuni  17909  filssufilg  17935  fmfnfmlem4  17981  trust  18251  elmopn2  18467  metrest  18546  dscopn  18613  metds0  18872  cncfmet  18930  negcncf  18940  iscmet2  19239  ovolfioo  19356  ovolficc  19357  itg1mulc  19588  ply1term  20115  plyconst  20117  reeff1olem  20354  usgraedgrnv  21389  ghsubgolem  21950  ocsh  22777  ocorth  22785  spansncvi  23146  pjss1coi  23658  sumdmdii  23910  measres  24568  measdivcstOLD  24570  measdivcst  24571  dya2iocuni  24625  dedekind  25179  dedekindle  25180  frrlem5e  25582  nobndlem2  25640  nobndlem6  25644  nobndlem8  25646  nobndup  25647  nobnddown  25648  nofulllem3  25651  nofulllem4  25652  nofulllem5  25653  opnrebl  26314  opnrebl2  26315  fness  26353  ssref  26354  comppfsc  26378  frinfm  26428  filbcmb  26433  nnubfi  26445  nninfnub  26446  sstotbnd3  26476  bndss  26486  exidreslem  26543  isidlc  26616  idlnegcl  26623  intidl  26630  unichnidl  26632  ssfz12  28088  ssfzo12  28113  lswrdcshw  28229  uhgraedgrnv  28255  snsslVD  28878  snssl  28879  sstrALT2VD  28883  sstrALT2  28884  suctrALTcf  28971  suctrALTcfVD  28972  bnj1190  29314  pmapglb2N  30505  elpaddn0  30534  paddasslem9  30562  paddasslem10  30563  pclfinN  30634  polval2N  30640  diaglbN  31790  dihord6apre  31991
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-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator