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

Theorem sstr2 3161
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 3149 . . . 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 2018 . 2  |-  ( A 
C_  B  ->  ( A. x ( x  e.  B  ->  x  e.  C )  ->  A. x
( x  e.  A  ->  x  e.  C ) ) )
4 dfss2 3144 . 2  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
5 dfss2 3144 . 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 3127
This theorem is referenced by:  sstr  3162  sstri  3163  sseq1  3174  sseq2  3175  ssun3  3315  ssun4  3316  ssinss1  3372  ssdisj  3479  triun  4100  trint0  4104  sspwb  4195  exss  4208  frss  4332  suceloni  4576  limsssuc  4613  relss  4763  funss  5212  funimass2  5264  fss  5335  tfrlem1  6359  oaordi  6512  oeworde  6559  nnaordi  6584  sbthlem1  6939  sbthlem2  6940  sbthlem3  6941  sbthlem6  6944  domunfican  7097  fiint  7101  fiss  7145  dffi3  7152  inf3lem1  7297  trcl  7378  tcss  7397  ac10ct  7629  ackbij2lem4  7836  cfslb  7860  cfslbn  7861  cfcoflem  7866  coftr  7867  fin23lem15  7928  fin23lem20  7931  fin23lem36  7942  isf32lem1  7947  axdc3lem2  8045  ttukeylem2  8105  wunex2  8328  tskcard  8371  mrcss  13480  isacs2  13517  lubss  14187  frmdss2  14447  lsmlub  14936  lsslss  15680  lspss  15703  aspss  16034  mplcoe1  16171  mplcoe2  16173  ocv2ss  16535  ocvsscon  16537  tgss  16668  tgcl  16669  tgss3  16686  clsss  16753  ntrss  16754  neiss  16808  ssnei2  16815  opnnei  16819  cnpnei  16955  cnpco  16958  cncls  16965  cnprest  16979  hauscmp  17096  1stcfb  17133  1stcelcls  17149  txcnpi  17264  txcnp  17276  txtube  17296  qtoptop2  17352  fgcl  17535  filssufilg  17568  ufileu  17576  uffix  17578  elfm2  17605  fmfnfmlem1  17611  fmco  17618  fbflim2  17634  flffbas  17652  flftg  17653  cnpflf2  17657  alexsubALTlem4  17706  neibl  18009  metcnp3  18048  xlebnum  18425  lebnumii  18426  caubl  18695  caublcls  18696  bcthlem2  18709  bcthlem5  18712  ovolsslem  18805  volsuplem  18874  dyadmbllem  18916  ellimc3  19191  limciun  19206  cpnord  19246  ubthlem1  21409  occon3  21836  chsupval  21874  chsupcl  21879  chsupss  21881  spanss  21887  chsupval2  21949  stlei  22780  dmdbr5  22848  mdsl0  22850  chrelat2i  22905  chirredlem1  22930  mdsymlem5  22947  mdsymlem6  22948  cvmliftlem15  23201  limsucncmpi  24259  inttrp  24474  inposet  24645  intopcoaconlem3b  24905  intopcoaconlem3  24906  exopcopn  24939  limptlimpr2lem2  24942  islimrs3  24948  lvsovso  24993  pgapspf  25419  clsint2  25614  reftr  25656  fgmin  25686  filnetlem4  25697  heiborlem1  25902  heiborlem8  25909  incssnn0  26153  islssfg2  26536  lindsss  26661  lsslinds  26668  hbtlem6  26700  sspwimpcf  27746  sspwimpcfVD  27747  sspwimpALT2  27755  pclssN  29250  dochexmidlem7  30823
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 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator