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

Theorem sstr2 3107
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 3097 . . . 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 2017 . 2  |-  ( A 
C_  B  ->  ( A. x ( x  e.  B  ->  x  e.  C )  ->  A. x
( x  e.  A  ->  x  e.  C ) ) )
4 dfss2 3092 . 2  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
5 dfss2 3092 . 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 1621    C_ wss 3078
This theorem is referenced by:  sstr  3108  sstri  3109  sseq1  3120  sseq2  3121  ssun3  3250  ssun4  3251  ssinss1  3304  ssdisj  3411  triun  4023  trint0  4027  sspwb  4117  exss  4129  frss  4253  suceloni  4495  limsssuc  4532  relss  4682  funss  5131  funimass2  5183  fss  5254  tfrlem1  6277  oaordi  6430  oeworde  6477  nnaordi  6502  sbthlem1  6856  sbthlem2  6857  sbthlem3  6858  sbthlem6  6861  domunfican  7014  fiint  7018  fiss  7061  dffi3  7068  inf3lem1  7213  trcl  7294  tcss  7313  ac10ct  7545  ackbij2lem4  7752  cfslb  7776  cfslbn  7777  cfcoflem  7782  coftr  7783  fin23lem15  7844  fin23lem20  7847  fin23lem36  7858  isf32lem1  7863  axdc3lem2  7961  ttukeylem2  8021  wunex2  8240  tskcard  8283  mrcss  13390  isacs2  13400  lubss  14069  frmdss2  14320  lsmlub  14809  lsslss  15553  lspss  15576  aspss  15904  mplcoe1  16041  mplcoe2  16043  ocv2ss  16405  ocvsscon  16407  tgss  16538  tgcl  16539  tgss3  16556  clsss  16623  ntrss  16624  neiss  16678  ssnei2  16685  opnnei  16689  cnpnei  16825  cnpco  16828  cncls  16835  cnprest  16849  hauscmp  16966  1stcfb  17003  1stcelcls  17019  txcnpi  17134  txcnp  17146  txtube  17166  qtoptop2  17222  fgcl  17405  filssufilg  17438  ufileu  17446  uffix  17448  elfm2  17475  fmfnfmlem1  17481  fmco  17488  fbflim2  17504  flffbas  17522  flftg  17523  cnpflf2  17527  alexsubALTlem4  17576  neibl  17879  metcnp3  17918  xlebnum  18295  lebnumii  18296  caubl  18565  caublcls  18566  bcthlem2  18579  bcthlem5  18582  ovolsslem  18675  volsuplem  18744  dyadmbllem  18786  ellimc3  19061  limciun  19076  cpnord  19116  ubthlem1  21279  occon3  21706  chsupval  21744  chsupcl  21749  chsupss  21751  spanss  21757  chsupval2  21819  stlei  22650  dmdbr5  22718  mdsl0  22720  chrelat2i  22775  chirredlem1  22800  mdsymlem5  22817  mdsymlem6  22818  cvmliftlem15  23000  limsucncmpi  24058  inttrp  24273  inposet  24444  intopcoaconlem3b  24704  intopcoaconlem3  24705  exopcopn  24738  limptlimpr2lem2  24741  islimrs3  24747  lvsovso  24792  pgapspf  25218  clsint2  25413  reftr  25455  fgmin  25485  filnetlem4  25496  heiborlem1  25701  heiborlem8  25708  incssnn0  25952  islssfg2  26335  lindsss  26460  lsslinds  26467  hbtlem6  26499  sspwimpcf  27386  sspwimpcfVD  27387  sspwimpALT2  27395  pclssN  28772  dochexmidlem7  30345
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator