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

Theorem ssel2 3287
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 3286 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 419 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1717    C_ wss 3264
This theorem is referenced by:  tz7.7  4549  onfr  4562  onmindif  4612  ordunisssuc  4625  onnmin  4724  onmindif2  4733  limsssuc  4771  ssimaex  5728  nssdmovg  6169  1st2nd  6333  boxriin  7041  ordunifi  7294  isfinite2  7302  ordtypelem7  7427  cnfcom  7591  coflim  8075  cflim2  8077  fin23lem11  8131  fin23lem26  8139  fin1a2lem13  8226  fpwwe2lem12  8450  suplem2pr  8864  axpre-sup  8978  axsup  9085  lbinfm  9894  dfinfmr  9918  infmrcl  9920  infmrlb  9922  uzwo  10472  uzwoOLD  10473  supminf  10496  lbzbi  10497  zsupss  10498  suprzcl2  10499  xrsupsslem  10818  xrinfmsslem  10819  xrub  10823  supxr2  10825  supxrun  10827  supxrunb1  10831  supxrbnd1  10833  supxrbnd2  10834  supxrub  10836  supxrbnd  10840  infmxrlb  10845  seqsplit  11284  shftlem  11811  rpnnen2lem10  12751  rpnnen2lem11  12752  gcdcllem1  12939  mrcuni  13774  isacs1i  13810  mreacs  13811  lubss  14476  gsumwspan  14719  subgint  14892  cntziinsn  15061  cntzsubg  15063  subrgint  15818  cntzsubr  15828  tgcl  16958  fctop  16992  cctop  16994  neips  17101  cmpsub  17386  1stcelcls  17446  txbasval  17560  fgss2  17828  filcon  17837  filuni  17839  filssufilg  17865  fmfnfmlem4  17911  trust  18181  elmopn2  18366  metrest  18445  dscopn  18493  metds0  18752  cncfmet  18810  negcncf  18820  iscmet2  19119  ovolfioo  19232  ovolficc  19233  itg1mulc  19464  ply1term  19991  plyconst  19993  reeff1olem  20230  usgraedgrnv  21265  ghsubgolem  21807  ocsh  22634  ocorth  22642  spansncvi  23003  pjss1coi  23515  sumdmdii  23767  measres  24371  measdivcstOLD  24373  measdivcst  24374  dya2iocuni  24428  dedekind  24967  dedekindle  24968  tfrALTlem  25301  frrlem5e  25314  nobndlem2  25372  nobndlem6  25376  nobndlem8  25378  nobndup  25379  nobnddown  25380  nofulllem3  25383  nofulllem4  25384  nofulllem5  25385  opnrebl  26015  opnrebl2  26016  fness  26054  ssref  26055  comppfsc  26079  frinfm  26129  filbcmb  26134  nnubfi  26146  nninfnub  26147  sstotbnd3  26177  bndss  26187  exidreslem  26244  isidlc  26317  idlnegcl  26324  intidl  26331  unichnidl  26333  snsslVD  28283  snssl  28284  sstrALT2VD  28288  sstrALT2  28289  suctrALTcf  28376  suctrALTcfVD  28377  bnj1190  28716  pmapglb2N  29886  elpaddn0  29915  paddasslem9  29943  paddasslem10  29944  pclfinN  30015  polval2N  30021  diaglbN  31171  dihord6apre  31372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-in 3271  df-ss 3278
  Copyright terms: Public domain W3C validator