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

Theorem ssel2 3499
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 3498 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 429 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  tz7.7  4904  onfr  4917  onmindif  4967  ordunisssuc  4980  ssimaex  5932  nssdmovg  6441  onnmin  6622  onmindif2  6631  limsssuc  6669  1st2nd  6830  f1o2ndf1  6891  boxriin  7511  ordunifi  7770  isfinite2  7778  ordtypelem7  7949  sucprcreg  8025  cnfcom  8144  cnfcomOLD  8152  coflim  8641  cflim2  8643  fin23lem11  8697  fin23lem26  8705  fin1a2lem13  8792  fpwwe2lem12  9019  suplem2pr  9431  axpre-sup  9546  axsup  9660  dedekind  9743  dedekindle  9744  lbinfm  10496  dfinfmr  10520  infmrcl  10522  infmrlb  10524  suprfinzcl  10975  uzwo  11144  uzwoOLD  11145  supminf  11169  lbzbi  11170  zsupss  11171  suprzcl2  11172  xrsupsslem  11498  xrinfmsslem  11499  xrub  11503  supxr2  11505  supxrun  11507  supxrunb1  11511  supxrbnd1  11513  supxrbnd2  11514  supxrub  11516  supxrbnd  11520  infmxrlb  11525  elfzom1elp1fzo  11851  ssfzo12  11873  fsuppmapnn0fiublem  12064  fsuppmapnn0fiub  12065  fsuppmapnn0fiub0  12067  seqsplit  12108  shftlem  12864  rpnnen2lem10  13818  rpnnen2lem11  13819  gcdcllem1  14008  mrcuni  14876  isacs1i  14912  mreacs  14913  lubss  15608  gsumwspan  15846  subgint  16030  cntziinsn  16177  cntzsubg  16179  pmtrdifellem4  16310  subrgint  17251  cntzsubr  17261  mdetunilem9  18917  tgcl  19265  fctop  19299  cctop  19301  neips  19408  cmpsub  19694  1stcelcls  19756  txbasval  19870  fgss2  20138  filcon  20147  filuni  20149  filssufilg  20175  fmfnfmlem4  20221  trust  20495  elmopn2  20711  metrest  20790  dscopn  20857  metds0  21117  cncfmet  21175  negcncf  21185  iscmet2  21496  ovolfioo  21642  ovolficc  21643  itg1mulc  21874  ply1term  22364  plyconst  22366  reeff1olem  22603  usgraedgrnv  24081  ghsubgolem  25076  ocsh  25905  ocorth  25913  spansncvi  26274  pjss1coi  26786  sumdmdii  27038  dfcnv2  27217  xrge0infss  27276  measres  27861  measdivcstOLD  27863  measdivcst  27864  dya2iocuni  27922  frrlem5e  29000  nobndlem2  29058  nobndlem6  29062  nobndlem8  29064  nobndup  29065  nobnddown  29066  nofulllem3  29069  nofulllem4  29070  nofulllem5  29071  fin2so  29645  opnrebl  29743  opnrebl2  29744  fness  29782  ssref  29783  comppfsc  29807  frinfm  29857  filbcmb  29862  nnubfi  29874  nninfnub  29875  sstotbnd3  29903  bndss  29913  exidreslem  29970  isidlc  30043  idlnegcl  30050  intidl  30057  unichnidl  30059  ssnel  31029  icccncfext  31254  fourierdlem87  31522  ssfz12  31825  uhgraedgrnv  31844  lindslinindimp2lem4  32161  lindslinindsimp2  32163  lincresunit3lem2  32180  lincresunit3  32181  snsslVD  32727  snssl  32728  sstrALT2VD  32732  sstrALT2  32733  suctrALTcf  32820  suctrALTcfVD  32821  bnj1190  33161  pmapglb2N  34585  elpaddn0  34614  paddasslem9  34642  paddasslem10  34643  pclfinN  34714  polval2N  34720  diaglbN  35870  dihord6apre  36071
  Copyright terms: Public domain W3C validator