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

Theorem ssel2 3332
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 3331 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
21imp 420 1  |-  ( ( A  C_  B  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1728    C_ wss 3309
This theorem is referenced by:  tz7.7  4642  onfr  4655  onmindif  4706  ordunisssuc  4719  onnmin  4818  onmindif2  4827  limsssuc  4865  ssimaex  5824  nssdmovg  6265  1st2nd  6429  f1o2ndf1  6490  boxriin  7140  ordunifi  7393  isfinite2  7401  ordtypelem7  7529  cnfcom  7693  coflim  8179  cflim2  8181  fin23lem11  8235  fin23lem26  8243  fin1a2lem13  8330  fpwwe2lem12  8554  suplem2pr  8968  axpre-sup  9082  axsup  9189  lbinfm  9999  dfinfmr  10023  infmrcl  10025  infmrlb  10027  uzwo  10577  uzwoOLD  10578  supminf  10601  lbzbi  10602  zsupss  10603  suprzcl2  10604  xrsupsslem  10923  xrinfmsslem  10924  xrub  10928  supxr2  10930  supxrun  10932  supxrunb1  10936  supxrbnd1  10938  supxrbnd2  10939  supxrub  10941  supxrbnd  10945  infmxrlb  10950  seqsplit  11394  shftlem  11921  rpnnen2lem10  12861  rpnnen2lem11  12862  gcdcllem1  13049  mrcuni  13884  isacs1i  13920  mreacs  13921  lubss  14586  gsumwspan  14829  subgint  15002  cntziinsn  15171  cntzsubg  15173  subrgint  15928  cntzsubr  15938  tgcl  17072  fctop  17106  cctop  17108  neips  17215  cmpsub  17501  1stcelcls  17562  txbasval  17676  fgss2  17944  filcon  17953  filuni  17955  filssufilg  17981  fmfnfmlem4  18027  trust  18297  elmopn2  18513  metrest  18592  dscopn  18659  metds0  18918  cncfmet  18976  negcncf  18986  iscmet2  19285  ovolfioo  19402  ovolficc  19403  itg1mulc  19632  ply1term  20161  plyconst  20163  reeff1olem  20400  usgraedgrnv  21435  ghsubgolem  21996  ocsh  22823  ocorth  22831  spansncvi  23192  pjss1coi  23704  sumdmdii  23956  measres  24611  measdivcstOLD  24613  measdivcst  24614  dya2iocuni  24668  dedekind  25222  dedekindle  25223  frrlem5e  25625  nobndlem2  25683  nobndlem6  25687  nobndlem8  25689  nobndup  25690  nobnddown  25691  nofulllem3  25694  nofulllem4  25695  nofulllem5  25696  opnrebl  26365  opnrebl2  26366  fness  26404  ssref  26405  comppfsc  26429  frinfm  26479  filbcmb  26484  nnubfi  26496  nninfnub  26497  sstotbnd3  26527  bndss  26537  exidreslem  26594  isidlc  26667  idlnegcl  26674  intidl  26681  unichnidl  26683  ssfz12  28225  ssfzo12  28251  lswrdcshw  28398  uhgraedgrnv  28424  snsslVD  29115  snssl  29116  sstrALT2VD  29120  sstrALT2  29121  suctrALTcf  29208  suctrALTcfVD  29209  bnj1190  29551  pmapglb2N  30742  elpaddn0  30771  paddasslem9  30799  paddasslem10  30800  pclfinN  30871  polval2N  30877  diaglbN  32027  dihord6apre  32228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3316  df-ss 3323
  Copyright terms: Public domain W3C validator