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

Theorem sstr2 3356
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ssel 3343 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 72 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  x  e.  C )  ->  ( x  e.  A  ->  x  e.  C ) ) )
32alimdv 1632 . 2  |-  ( A 
C_  B  ->  ( A. x ( x  e.  B  ->  x  e.  C )  ->  A. x
( x  e.  A  ->  x  e.  C ) ) )
4 dfss2 3338 . 2  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
5 dfss2 3338 . 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 4   A.wal 1550    e. wcel 1726    C_ wss 3321
This theorem is referenced by:  sstr  3357  sstri  3358  sseq1  3370  sseq2  3371  ssun3  3513  ssun4  3514  ssinss1  3570  ssdisj  3678  triun  4316  trint0  4320  sspwb  4414  exss  4427  frss  4550  suceloni  4794  limsssuc  4831  relss  4964  funss  5473  funimass2  5528  fss  5600  tfrlem1  6637  oaordi  6790  oeworde  6837  nnaordi  6862  sbthlem2  7219  sbthlem3  7220  sbthlem6  7223  domunfican  7380  fiint  7384  fiss  7430  dffi3  7437  inf3lem1  7584  trcl  7665  tcss  7684  ac10ct  7916  ackbij2lem4  8123  cfslb  8147  cfslbn  8148  cfcoflem  8153  coftr  8154  fin23lem15  8215  fin23lem20  8218  fin23lem36  8229  isf32lem1  8234  axdc3lem2  8332  ttukeylem2  8391  wunex2  8614  tskcard  8657  mrcss  13842  isacs2  13879  lubss  14549  frmdss2  14809  lsmlub  15298  lsslss  16038  lspss  16061  aspss  16392  mplcoe1  16529  mplcoe2  16531  ocv2ss  16901  ocvsscon  16903  tgss  17034  tgcl  17035  tgss3  17052  clsss  17119  ntrss  17120  neiss  17174  ssnei2  17181  opnnei  17185  cnpnei  17329  cnpco  17332  cncls  17339  cnprest  17354  hauscmp  17471  1stcfb  17509  1stcelcls  17525  txcnpi  17641  txcnp  17653  txtube  17673  qtoptop2  17732  fgcl  17911  filssufilg  17944  ufileu  17952  uffix  17954  elfm2  17981  fmfnfmlem1  17987  fmco  17994  fbflim2  18010  flffbas  18028  flftg  18029  cnpflf2  18033  alexsubALTlem4  18082  neibl  18532  metcnp3  18571  xlebnum  18991  lebnumii  18992  caubl  19261  caublcls  19262  bcthlem2  19279  bcthlem5  19282  ovolsslem  19381  volsuplem  19450  dyadmbllem  19492  ellimc3  19767  limciun  19782  cpnord  19822  ubthlem1  22373  occon3  22800  chsupval  22838  chsupcl  22843  chsupss  22845  spanss  22851  chsupval2  22913  stlei  23744  dmdbr5  23812  mdsl0  23814  chrelat2i  23869  chirredlem1  23894  mdsymlem5  23911  mdsymlem6  23912  cvmliftlem15  24986  limsucncmpi  26196  clsint2  26333  reftr  26370  fgmin  26400  filnetlem4  26411  heiborlem1  26521  heiborlem8  26528  incssnn0  26766  islssfg2  27147  lindsss  27272  lsslinds  27279  hbtlem6  27311  sspwimpcf  29033  sspwimpcfVD  29034  pclssN  30692  dochexmidlem7  32265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-in 3328  df-ss 3335
  Copyright terms: Public domain W3C validator