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

Theorem ssel2 3188
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 3187 . 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 1696    C_ wss 3165
This theorem is referenced by:  tz7.7  4434  onfr  4447  onmindif  4498  ordunisssuc  4511  onnmin  4610  onmindif2  4619  limsssuc  4657  ssimaex  5600  1st2nd  6182  boxriin  6874  ordunifi  7123  isfinite2  7131  ordtypelem7  7255  cnfcom  7419  coflim  7903  cflim2  7905  fin23lem11  7959  fin23lem26  7967  fin1a2lem13  8054  fpwwe2lem12  8279  suplem2pr  8693  axpre-sup  8807  axsup  8914  lbinfm  9723  dfinfmr  9747  infmrcl  9749  infmrlb  9751  uzwo  10297  uzwoOLD  10298  supminf  10321  lbzbi  10322  zsupss  10323  suprzcl2  10324  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxr2  10648  supxrun  10650  supxrunb1  10654  supxrbnd1  10656  supxrbnd2  10657  supxrub  10659  supxrbnd  10663  infmxrlb  10668  seqsplit  11095  shftlem  11579  rpnnen2lem10  12518  rpnnen2lem11  12519  gcdcllem1  12706  mrcuni  13539  isacs1i  13575  mreacs  13576  lubss  14241  gsumwspan  14484  subgint  14657  cntziinsn  14826  cntzsubg  14828  subrgint  15583  cntzsubr  15593  tgcl  16723  fctop  16757  cctop  16759  neips  16866  cmpsub  17143  1stcelcls  17203  txbasval  17317  fgss2  17585  filcon  17594  filuni  17596  filssufilg  17622  fmfnfmlem4  17668  elmopn2  18007  metrest  18086  dscopn  18112  metds0  18370  cncfmet  18428  negcncf  18437  iscmet2  18736  ovolfioo  18843  ovolficc  18844  itg1mulc  19075  ply1term  19602  plyconst  19604  reeff1olem  19838  ghsubgolem  21053  ocsh  21878  ocorth  21886  spansncvi  22247  pjss1coi  22759  sumdmdii  23011  opfv  23206  xrofsup  23270  elsigass  23501  measres  23564  measdivcstOLD  23566  measdivcst  23567  dedekind  24097  dedekindle  24098  tfrALTlem  24347  frrlem5e  24360  nobndlem2  24418  nobndlem6  24422  nobndlem8  24424  nobndup  24425  nobnddown  24426  nofulllem3  24429  nofulllem4  24430  nofulllem5  24431  npincppr  25262  prodeqfv  25421  lvsovso  25729  intvconlem1  25806  opnrebl  26338  opnrebl2  26339  fness  26385  ssref  26386  comppfsc  26410  frinfm  26519  filbcmb  26535  nnubfi  26563  nninfnub  26564  sstotbnd3  26603  bndss  26613  exidreslem  26670  isidlc  26743  idlnegcl  26750  intidl  26757  unichnidl  26759  ubelsupr  27794  fmul01  27813  fmulcl  27814  stoweidlem5  27857  stoweidlem7  27859  stoweidlem11  27863  stoweidlem17  27869  stoweidlem26  27878  stoweidlem31  27883  stoweidlem36  27888  stoweidlem43  27895  stoweidlem44  27896  stoweidlem51  27903  stoweidlem52  27904  stoweidlem60  27912  stoweid  27915  nssdmovg  28194  usgraedgrnv  28257  snsslVD  28920  snssl  28921  sstrALT2VD  28926  sstrALT2  28927  suctrALTcf  29014  suctrALTcfVD  29015  suctrALT4  29020  bnj1190  29354  pmapglb2N  30582  elpaddn0  30611  paddasslem9  30639  paddasslem10  30640  pclfinN  30711  polval2N  30717  diaglbN  31867  dihord6apre  32068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator