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

Theorem ssel2 3303
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 3302 . 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 1721    C_ wss 3280
This theorem is referenced by:  tz7.7  4567  onfr  4580  onmindif  4630  ordunisssuc  4643  onnmin  4742  onmindif2  4751  limsssuc  4789  ssimaex  5747  nssdmovg  6188  1st2nd  6352  f1o2ndf1  6413  boxriin  7063  ordunifi  7316  isfinite2  7324  ordtypelem7  7449  cnfcom  7613  coflim  8097  cflim2  8099  fin23lem11  8153  fin23lem26  8161  fin1a2lem13  8248  fpwwe2lem12  8472  suplem2pr  8886  axpre-sup  9000  axsup  9107  lbinfm  9917  dfinfmr  9941  infmrcl  9943  infmrlb  9945  uzwo  10495  uzwoOLD  10496  supminf  10519  lbzbi  10520  zsupss  10521  suprzcl2  10522  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxr2  10848  supxrun  10850  supxrunb1  10854  supxrbnd1  10856  supxrbnd2  10857  supxrub  10859  supxrbnd  10863  infmxrlb  10868  seqsplit  11311  shftlem  11838  rpnnen2lem10  12778  rpnnen2lem11  12779  gcdcllem1  12966  mrcuni  13801  isacs1i  13837  mreacs  13838  lubss  14503  gsumwspan  14746  subgint  14919  cntziinsn  15088  cntzsubg  15090  subrgint  15845  cntzsubr  15855  tgcl  16989  fctop  17023  cctop  17025  neips  17132  cmpsub  17417  1stcelcls  17477  txbasval  17591  fgss2  17859  filcon  17868  filuni  17870  filssufilg  17896  fmfnfmlem4  17942  trust  18212  elmopn2  18428  metrest  18507  dscopn  18574  metds0  18833  cncfmet  18891  negcncf  18901  iscmet2  19200  ovolfioo  19317  ovolficc  19318  itg1mulc  19549  ply1term  20076  plyconst  20078  reeff1olem  20315  usgraedgrnv  21350  ghsubgolem  21911  ocsh  22738  ocorth  22746  spansncvi  23107  pjss1coi  23619  sumdmdii  23871  measres  24529  measdivcstOLD  24531  measdivcst  24532  dya2iocuni  24586  dedekind  25140  dedekindle  25141  tfrALTlem  25490  frrlem5e  25503  nobndlem2  25561  nobndlem6  25565  nobndlem8  25567  nobndup  25568  nobnddown  25569  nofulllem3  25572  nofulllem4  25573  nofulllem5  25574  opnrebl  26213  opnrebl2  26214  fness  26252  ssref  26253  comppfsc  26277  frinfm  26327  filbcmb  26332  nnubfi  26344  nninfnub  26345  sstotbnd3  26375  bndss  26385  exidreslem  26442  isidlc  26515  idlnegcl  26522  intidl  26529  unichnidl  26531  ssfz12  27976  ssfzo12  27990  uhgraedgrnv  28032  snsslVD  28650  snssl  28651  sstrALT2VD  28655  sstrALT2  28656  suctrALTcf  28743  suctrALTcfVD  28744  bnj1190  29083  pmapglb2N  30253  elpaddn0  30282  paddasslem9  30310  paddasslem10  30311  pclfinN  30382  polval2N  30388  diaglbN  31538  dihord6apre  31739
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator