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

Theorem ssel2 3175
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 3174 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 418 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  tz7.7  4418  onfr  4431  onmindif  4482  ordunisssuc  4495  onnmin  4594  onmindif2  4603  limsssuc  4641  ssimaex  5584  1st2nd  6166  boxriin  6858  ordunifi  7107  isfinite2  7115  ordtypelem7  7239  cnfcom  7403  coflim  7887  cflim2  7889  fin23lem11  7943  fin23lem26  7951  fin1a2lem13  8038  fpwwe2lem12  8263  suplem2pr  8677  axpre-sup  8791  axsup  8898  lbinfm  9707  dfinfmr  9731  infmrcl  9733  infmrlb  9735  uzwo  10281  uzwoOLD  10282  supminf  10305  lbzbi  10306  zsupss  10307  suprzcl2  10308  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxr2  10632  supxrun  10634  supxrunb1  10638  supxrbnd1  10640  supxrbnd2  10641  supxrub  10643  supxrbnd  10647  infmxrlb  10652  seqsplit  11079  shftlem  11563  rpnnen2lem10  12502  rpnnen2lem11  12503  gcdcllem1  12690  mrcuni  13523  isacs1i  13559  mreacs  13560  lubss  14225  gsumwspan  14468  subgint  14641  cntziinsn  14810  cntzsubg  14812  subrgint  15567  cntzsubr  15577  tgcl  16707  fctop  16741  cctop  16743  neips  16850  cmpsub  17127  1stcelcls  17187  txbasval  17301  fgss2  17569  filcon  17578  filuni  17580  filssufilg  17606  fmfnfmlem4  17652  elmopn2  17991  metrest  18070  dscopn  18096  metds0  18354  cncfmet  18412  negcncf  18421  iscmet2  18720  ovolfioo  18827  ovolficc  18828  itg1mulc  19059  ply1term  19586  plyconst  19588  reeff1olem  19822  ghsubgolem  21037  ocsh  21862  ocorth  21870  spansncvi  22231  pjss1coi  22743  sumdmdii  22995  opfv  23190  xrofsup  23255  elsigass  23486  measres  23549  measdivcstOLD  23551  measdivcst  23552  dedekind  24082  dedekindle  24083  tfrALTlem  24276  frrlem5e  24289  nobndlem2  24347  nobndlem6  24351  nobndlem8  24353  nobndup  24354  nobnddown  24355  nofulllem3  24358  nofulllem4  24359  nofulllem5  24360  npincppr  25159  prodeqfv  25318  lvsovso  25626  intvconlem1  25703  opnrebl  26235  opnrebl2  26236  fness  26282  ssref  26283  comppfsc  26307  frinfm  26416  filbcmb  26432  nnubfi  26460  nninfnub  26461  sstotbnd3  26500  bndss  26510  exidreslem  26567  isidlc  26640  idlnegcl  26647  intidl  26654  unichnidl  26656  ubelsupr  27691  fmul01  27710  fmulcl  27711  stoweidlem5  27754  stoweidlem7  27756  stoweidlem11  27760  stoweidlem17  27766  stoweidlem26  27775  stoweidlem31  27780  stoweidlem36  27785  stoweidlem43  27792  stoweidlem44  27793  stoweidlem51  27800  stoweidlem52  27801  stoweidlem60  27809  stoweid  27812  nssdmovg  28077  usgraedgrnv  28123  snsslVD  28604  snssl  28605  sstrALT2VD  28610  sstrALT2  28611  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT4  28704  bnj1190  29038  pmapglb2N  29960  elpaddn0  29989  paddasslem9  30017  paddasslem10  30018  pclfinN  30089  polval2N  30095  diaglbN  31245  dihord6apre  31446
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator