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

Theorem sstr2 3186
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 3174 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 69 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  x  e.  C )  ->  ( x  e.  A  ->  x  e.  C ) ) )
32alimdv 1607 . 2  |-  ( A 
C_  B  ->  ( A. x ( x  e.  B  ->  x  e.  C )  ->  A. x
( x  e.  A  ->  x  e.  C ) ) )
4 dfss2 3169 . 2  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
5 dfss2 3169 . 2  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
63, 4, 53imtr4g 261 1  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  sstr  3187  sstri  3188  sseq1  3199  sseq2  3200  ssun3  3340  ssun4  3341  ssinss1  3397  ssdisj  3504  triun  4126  trint0  4130  sspwb  4223  exss  4236  frss  4360  suceloni  4604  limsssuc  4641  relss  4775  funss  5273  funimass2  5326  fss  5397  tfrlem1  6391  oaordi  6544  oeworde  6591  nnaordi  6616  sbthlem1  6971  sbthlem2  6972  sbthlem3  6973  sbthlem6  6976  domunfican  7129  fiint  7133  fiss  7177  dffi3  7184  inf3lem1  7329  trcl  7410  tcss  7429  ac10ct  7661  ackbij2lem4  7868  cfslb  7892  cfslbn  7893  cfcoflem  7898  coftr  7899  fin23lem15  7960  fin23lem20  7963  fin23lem36  7974  isf32lem1  7979  axdc3lem2  8077  ttukeylem2  8137  wunex2  8360  tskcard  8403  mrcss  13518  isacs2  13555  lubss  14225  frmdss2  14485  lsmlub  14974  lsslss  15718  lspss  15741  aspss  16072  mplcoe1  16209  mplcoe2  16211  ocv2ss  16573  ocvsscon  16575  tgss  16706  tgcl  16707  tgss3  16724  clsss  16791  ntrss  16792  neiss  16846  ssnei2  16853  opnnei  16857  cnpnei  16993  cnpco  16996  cncls  17003  cnprest  17017  hauscmp  17134  1stcfb  17171  1stcelcls  17187  txcnpi  17302  txcnp  17314  txtube  17334  qtoptop2  17390  fgcl  17573  filssufilg  17606  ufileu  17614  uffix  17616  elfm2  17643  fmfnfmlem1  17649  fmco  17656  fbflim2  17672  flffbas  17690  flftg  17691  cnpflf2  17695  alexsubALTlem4  17744  neibl  18047  metcnp3  18086  xlebnum  18463  lebnumii  18464  caubl  18733  caublcls  18734  bcthlem2  18747  bcthlem5  18750  ovolsslem  18843  volsuplem  18912  dyadmbllem  18954  ellimc3  19229  limciun  19244  cpnord  19284  ubthlem1  21449  occon3  21876  chsupval  21914  chsupcl  21919  chsupss  21921  spanss  21927  chsupval2  21989  stlei  22820  dmdbr5  22888  mdsl0  22890  chrelat2i  22945  chirredlem1  22970  mdsymlem5  22987  mdsymlem6  22988  cvmliftlem15  23829  limsucncmpi  24884  inttrp  25108  inposet  25278  intopcoaconlem3b  25538  intopcoaconlem3  25539  exopcopn  25572  limptlimpr2lem2  25575  islimrs3  25581  lvsovso  25626  pgapspf  26052  clsint2  26247  reftr  26289  fgmin  26319  filnetlem4  26330  heiborlem1  26535  heiborlem8  26542  incssnn0  26786  islssfg2  27169  lindsss  27294  lsslinds  27301  hbtlem6  27333  sspwimpcf  28696  sspwimpcfVD  28697  sspwimpALT2  28705  pclssN  30083  dochexmidlem7  31656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator