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

Theorem ssel2 3348
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 3347 . 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 1761    C_ wss 3325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339
This theorem is referenced by:  tz7.7  4741  onfr  4754  onmindif  4804  ordunisssuc  4817  ssimaex  5753  nssdmovg  6244  onnmin  6413  onmindif2  6422  limsssuc  6460  1st2nd  6619  f1o2ndf1  6679  boxriin  7301  ordunifi  7558  isfinite2  7566  ordtypelem7  7734  sucprcreg  7810  cnfcom  7929  cnfcomOLD  7937  coflim  8426  cflim2  8428  fin23lem11  8482  fin23lem26  8490  fin1a2lem13  8577  fpwwe2lem12  8804  suplem2pr  9218  axpre-sup  9332  axsup  9446  dedekind  9529  dedekindle  9530  lbinfm  10279  dfinfmr  10303  infmrcl  10305  infmrlb  10307  uzwo  10913  uzwoOLD  10914  supminf  10938  lbzbi  10939  zsupss  10940  suprzcl2  10941  xrsupsslem  11265  xrinfmsslem  11266  xrub  11270  supxr2  11272  supxrun  11274  supxrunb1  11278  supxrbnd1  11280  supxrbnd2  11281  supxrub  11283  supxrbnd  11287  infmxrlb  11292  ssfzo12  11616  seqsplit  11835  shftlem  12553  rpnnen2lem10  13502  rpnnen2lem11  13503  gcdcllem1  13691  mrcuni  14555  isacs1i  14591  mreacs  14592  lubss  15287  gsumwspan  15517  subgint  15698  cntziinsn  15845  cntzsubg  15847  pmtrdifellem4  15978  subrgint  16867  cntzsubr  16877  mdetunilem9  18326  tgcl  18474  fctop  18508  cctop  18510  neips  18617  cmpsub  18903  1stcelcls  18965  txbasval  19079  fgss2  19347  filcon  19356  filuni  19358  filssufilg  19384  fmfnfmlem4  19430  trust  19704  elmopn2  19920  metrest  19999  dscopn  20066  metds0  20326  cncfmet  20384  negcncf  20394  iscmet2  20705  ovolfioo  20851  ovolficc  20852  itg1mulc  21082  ply1term  21615  plyconst  21617  reeff1olem  21854  usgraedgrnv  23215  ghsubgolem  23776  ocsh  24605  ocorth  24613  spansncvi  24974  pjss1coi  25486  sumdmdii  25738  dfcnv2  25913  measres  26556  measdivcstOLD  26558  measdivcst  26559  dya2iocuni  26618  frrlem5e  27689  nobndlem2  27747  nobndlem6  27751  nobndlem8  27753  nobndup  27754  nobnddown  27755  nofulllem3  27758  nofulllem4  27759  nofulllem5  27760  fin2so  28325  opnrebl  28424  opnrebl2  28425  fness  28463  ssref  28464  comppfsc  28488  frinfm  28538  filbcmb  28543  nnubfi  28555  nninfnub  28556  sstotbnd3  28584  bndss  28594  exidreslem  28651  isidlc  28724  idlnegcl  28731  intidl  28738  unichnidl  28740  ssfz12  30106  uhgraedgrnv  30182  lindslinindimp2lem4  30819  lindslinindsimp2  30821  lincresunit3lem2  30838  lincresunit3  30839  snsslVD  31382  snssl  31383  sstrALT2VD  31387  sstrALT2  31388  suctrALTcf  31475  suctrALTcfVD  31476  bnj1190  31816  pmapglb2N  33103  elpaddn0  33132  paddasslem9  33160  paddasslem10  33161  pclfinN  33232  polval2N  33238  diaglbN  34388  dihord6apre  34589
  Copyright terms: Public domain W3C validator