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

Theorem ssel2 3484
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 3483 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 427 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  tz7.7  4893  onfr  4906  onmindif  4956  ordunisssuc  4969  ssimaex  5913  nssdmovg  6430  onnmin  6611  onmindif2  6620  limsssuc  6658  1st2nd  6819  f1o2ndf1  6881  boxriin  7504  ordunifi  7762  isfinite2  7770  ordtypelem7  7941  sucprcreg  8017  cnfcom  8135  cnfcomOLD  8143  coflim  8632  cflim2  8634  fin23lem11  8688  fin23lem26  8696  fin1a2lem13  8783  fpwwe2lem12  9008  suplem2pr  9420  axpre-sup  9535  axsup  9649  dedekind  9733  dedekindle  9734  lbinfm  10491  dfinfmr  10515  infmrcl  10517  infmrlb  10519  suprfinzcl  10975  uzwo  11145  uzwoOLD  11146  supminf  11170  lbzbi  11171  zsupss  11172  suprzcl2  11173  xrsupsslem  11501  xrinfmsslem  11502  xrub  11506  supxr2  11508  supxrun  11510  supxrunb1  11514  supxrbnd1  11516  supxrbnd2  11517  supxrub  11519  supxrbnd  11523  infmxrlb  11528  elfzom1elp1fzo  11864  ssfzo12  11886  fsuppmapnn0fiublem  12081  fsuppmapnn0fiub  12082  fsuppmapnn0fiub0  12084  seqsplit  12125  shftlem  12986  rpnnen2lem10  14044  rpnnen2lem11  14045  gcdcllem1  14236  mrcuni  15113  isacs1i  15149  mreacs  15150  lubss  15953  gsumwspan  16216  subgint  16427  cntziinsn  16574  cntzsubg  16576  pmtrdifellem4  16706  subrgint  17649  cntzsubr  17659  mdetunilem9  19292  tgcl  19641  fctop  19675  cctop  19677  neips  19784  cmpsub  20070  1stcelcls  20131  ssref  20182  comppfsc  20202  txbasval  20276  fgss2  20544  filcon  20553  filuni  20555  filssufilg  20581  fmfnfmlem4  20627  trust  20901  elmopn2  21117  metrest  21196  dscopn  21263  metds0  21523  cncfmet  21581  negcncf  21591  iscmet2  21902  ovolfioo  22048  ovolficc  22049  itg1mulc  22280  ply1term  22770  plyconst  22772  reeff1olem  23010  usgraedgrnv  24582  ghsubgolemOLD  25573  ocsh  26402  ocorth  26410  spansncvi  26771  pjss1coi  27283  sumdmdii  27535  dfcnv2  27748  xrge0infss  27814  measres  28433  measdivcstOLD  28435  measdivcst  28436  dya2iocuni  28494  frrlem5e  29638  nobndlem2  29696  nobndlem6  29700  nobndlem8  29702  nobndup  29703  nobnddown  29704  nofulllem3  29707  nofulllem4  29708  nofulllem5  29709  fin2so  30283  opnrebl  30381  opnrebl2  30382  fness  30410  frinfm  30469  filbcmb  30474  nnubfi  30486  nninfnub  30487  sstotbnd3  30515  bndss  30525  exidreslem  30582  isidlc  30655  idlnegcl  30662  intidl  30669  unichnidl  30671  ssnel  31665  ssfz12  32723  uhgraedgrnv  32740  lindslinindimp2lem4  33335  lindslinindsimp2  33337  lincresunit3lem2  33354  lincresunit3  33355  snsslVD  34048  snssl  34049  sstrALT2VD  34053  sstrALT2  34054  suctrALTcf  34142  suctrALTcfVD  34143  bnj1190  34484  pmapglb2N  35911  elpaddn0  35940  paddasslem9  35968  paddasslem10  35969  pclfinN  36040  polval2N  36046  diaglbN  37198  dihord6apre  37399
  Copyright terms: Public domain W3C validator