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

Theorem sstr2 3187
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
sstr2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )

Proof of Theorem sstr2
StepHypRef Expression
1 ssel 3175 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 71 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  x  e.  C )  ->  ( x  e.  A  ->  x  e.  C ) ) )
32alimdv 1612 . 2  |-  ( A 
C_  B  ->  ( A. x ( x  e.  B  ->  x  e.  C )  ->  A. x
( x  e.  A  ->  x  e.  C ) ) )
4 dfss2 3170 . 2  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
5 dfss2 3170 . 2  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
63, 4, 53imtr4g 263 1  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532    e. wcel 1688    C_ wss 3153
This theorem is referenced by:  sstr  3188  sstri  3189  sseq1  3200  sseq2  3201  ssun3  3341  ssun4  3342  ssinss1  3398  ssdisj  3505  triun  4127  trint0  4131  sspwb  4222  exss  4235  frss  4359  suceloni  4603  limsssuc  4640  relss  4774  funss  5239  funimass2  5291  fss  5362  tfrlem1  6386  oaordi  6539  oeworde  6586  nnaordi  6611  sbthlem1  6966  sbthlem2  6967  sbthlem3  6968  sbthlem6  6971  domunfican  7124  fiint  7128  fiss  7172  dffi3  7179  inf3lem1  7324  trcl  7405  tcss  7424  ac10ct  7656  ackbij2lem4  7863  cfslb  7887  cfslbn  7888  cfcoflem  7893  coftr  7894  fin23lem15  7955  fin23lem20  7958  fin23lem36  7969  isf32lem1  7974  axdc3lem2  8072  ttukeylem2  8132  wunex2  8355  tskcard  8398  mrcss  13512  isacs2  13549  lubss  14219  frmdss2  14479  lsmlub  14968  lsslss  15712  lspss  15735  aspss  16066  mplcoe1  16203  mplcoe2  16205  ocv2ss  16567  ocvsscon  16569  tgss  16700  tgcl  16701  tgss3  16718  clsss  16785  ntrss  16786  neiss  16840  ssnei2  16847  opnnei  16851  cnpnei  16987  cnpco  16990  cncls  16997  cnprest  17011  hauscmp  17128  1stcfb  17165  1stcelcls  17181  txcnpi  17296  txcnp  17308  txtube  17328  qtoptop2  17384  fgcl  17567  filssufilg  17600  ufileu  17608  uffix  17610  elfm2  17637  fmfnfmlem1  17643  fmco  17650  fbflim2  17666  flffbas  17684  flftg  17685  cnpflf2  17689  alexsubALTlem4  17738  neibl  18041  metcnp3  18080  xlebnum  18457  lebnumii  18458  caubl  18727  caublcls  18728  bcthlem2  18741  bcthlem5  18744  ovolsslem  18837  volsuplem  18906  dyadmbllem  18948  ellimc3  19223  limciun  19238  cpnord  19278  ubthlem1  21441  occon3  21868  chsupval  21906  chsupcl  21911  chsupss  21913  spanss  21919  chsupval2  21981  stlei  22812  dmdbr5  22880  mdsl0  22882  chrelat2i  22937  chirredlem1  22962  mdsymlem5  22979  mdsymlem6  22980  cvmliftlem15  23233  limsucncmpi  24291  inttrp  24506  inposet  24677  intopcoaconlem3b  24937  intopcoaconlem3  24938  exopcopn  24971  limptlimpr2lem2  24974  islimrs3  24980  lvsovso  25025  pgapspf  25451  clsint2  25646  reftr  25688  fgmin  25718  filnetlem4  25729  heiborlem1  25934  heiborlem8  25941  incssnn0  26185  islssfg2  26568  lindsss  26693  lsslinds  26700  hbtlem6  26732  sspwimpcf  27964  sspwimpcfVD  27965  sspwimpALT2  27973  pclssN  29350  dochexmidlem7  30923
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator