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

Theorem ssel2 3438
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 3437 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 435 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1897    C_ wss 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429
This theorem is referenced by:  tz7.7  5467  onfr  5480  onmindif  5530  ordunisssuc  5543  ssimaex  5952  nssdmovg  6477  onnmin  6656  onmindif2  6665  limsssuc  6703  1st2nd  6865  f1o2ndf1  6930  dfrecs3  7116  boxriin  7589  ordunifi  7846  isfinite2  7854  ordtypelem7  8064  sucprcreg  8139  cnfcom  8230  coflim  8716  cflim2  8718  fin23lem11  8772  fin23lem26  8780  fin1a2lem13  8867  fpwwe2lem12  9091  suplem2pr  9503  axpre-sup  9618  axsup  9734  dedekind  9822  dedekindle  9823  lbinf  10586  lbinfmOLD  10587  dfinfre  10615  dfinfmrOLD  10616  infmrclOLD  10620  infrelb  10623  infmrlbOLD  10624  suprfinzcl  11078  uzwo  11250  supminf  11278  supminfOLD  11279  lbzbi  11280  zsupss  11281  suprzcl2  11282  xrsupsslem  11620  xrinfmsslem  11621  xrub  11625  supxr2  11627  supxrun  11629  supxrunb1  11633  supxrbnd1  11635  supxrbnd2  11636  supxrub  11638  supxrbnd  11642  infxrlb  11648  infmxrlbOLD  11652  elfzom1elp1fzo  12011  ssfzo12  12034  fsuppmapnn0fiublem  12233  fsuppmapnn0fiub  12234  fsuppmapnn0fiub0  12236  seqsplit  12277  shftlem  13179  rpnnen2lem10  14324  rpnnen2lem11  14325  gcdcllem1  14521  mrcuni  15575  isacs1i  15611  mreacs  15612  lubss  16415  gsumwspan  16678  subgint  16889  cntziinsn  17036  cntzsubg  17038  pmtrdifellem4  17168  subrgint  18078  cntzsubr  18088  mdetunilem9  19693  tgcl  20033  fctop  20067  cctop  20069  neips  20177  cmpsub  20463  1stcelcls  20524  ssref  20575  comppfsc  20595  txbasval  20669  fgss2  20937  filcon  20946  filuni  20948  filssufilg  20974  fmfnfmlem4  21020  trust  21292  elmopn2  21508  metrest  21587  dscopn  21636  metds0  21915  metds0OLD  21930  cncfmet  21988  negcncf  21998  iscmet2  22312  ovolfioo  22468  ovolficc  22469  itg1mulc  22710  ply1term  23206  plyconst  23208  reeff1olem  23449  usgraedgrnv  25152  ghsubgolemOLD  26146  ocsh  26984  ocorth  26992  spansncvi  27353  pjss1coi  27864  sumdmdii  28116  dfcnv2  28327  xrge0infss  28388  xrge0infssOLD  28389  measres  29092  measdivcstOLD  29094  measdivcst  29095  dya2iocuni  29153  bnj1190  29865  frrlem5e  30570  nobndlem2  30630  nobndlem6  30634  nobndlem8  30636  nobndup  30637  nobnddown  30638  nofulllem3  30641  nofulllem4  30642  nofulllem5  30643  opnrebl  31024  opnrebl2  31025  fness  31053  fin2so  31976  poimirlem27  32011  poimir  32017  frinfm  32106  filbcmb  32111  nnubfi  32123  nninfnub  32124  sstotbnd3  32152  bndss  32162  exidreslem  32219  isidlc  32292  idlnegcl  32299  intidl  32306  unichnidl  32308  pmapglb2N  33380  elpaddn0  33409  paddasslem9  33437  paddasslem10  33438  pclfinN  33509  polval2N  33515  diaglbN  34667  dihord6apre  34868  snsslVD  37264  snssl  37265  sstrALT2VD  37269  sstrALT2  37270  suctrALTcf  37358  suctrALTcfVD  37359  ssnel  37405  uzwo4  37429  sge0iunmptlemfi  38292  caratheodorylem2  38385  ovnlerp  38421  ssfz12  39095  usgruspgrb  39315  uhgraedgrnv  39935  lindslinindimp2lem4  40526  lindslinindsimp2  40528  lincresunit3lem2  40545  lincresunit3  40546
  Copyright terms: Public domain W3C validator