Theorem sstr2 3363

Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-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.

Step	Hyp	Ref	Expression
1		ssel 3350	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	imim1d 75	. . 3 |- ( A C_ B -> ( ( x e. B -> x e. C ) -> ( x e. A -> x e. C ) ) )
3	2	alimdv 1675	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3345	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3345	. 2 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6	3, 4, 5	3imtr4g 270	1 |- ( A C_ B -> ( B C_ C -> A C_ C ) )

Syntax hints:   -> wi 4   A.wal 1367   e. wcel 1756   C_ wss 3328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342

This theorem is referenced by:  sstr  3364  sstri  3365  sseq1  3377  sseq2  3378  ssun3  3521  ssun4  3522  ssinss1  3578  ssdisj  3728  triun  4398  trint0  4402  sspwb  4541  exss  4555  frss  4687  relss  4927  funss  5436  funimass2  5492  fss  5567  suceloni  6424  limsssuc  6461  oaordi  6985  oeworde  7032  nnaordi  7057  sbthlem2  7422  sbthlem3  7423  sbthlem6  7426  domunfican  7584  fiint  7588  fiss  7674  dffi3  7681  inf3lem1  7834  trcl  7948  tcss  7964  ac10ct  8204  ackbij2lem4  8411  cfslb  8435  cfslbn  8436  cfcoflem  8441  coftr  8442  fin23lem15  8503  fin23lem20  8506  fin23lem36  8517  isf32lem1  8522  axdc3lem2  8620  ttukeylem2  8679  wunex2  8905  tskcard  8948  mrcss  14554  isacs2  14591  lubss  15291  frmdss2  15541  lsmlub  16162  lsslss  17042  lspss  17065  aspss  17403  mplcoe1  17544  mplcoe5  17548  mplcoe2OLD  17550  ocv2ss  18098  ocvsscon  18100  lindsss  18253  lsslinds  18260  mdetunilem9  18426  tgss  18573  tgcl  18574  tgss3  18591  clsss  18658  ntrss  18659  neiss  18713  ssnei2  18720  opnnei  18724  cnpnei  18868  cnpco  18871  cncls  18878  cnprest  18893  hauscmp  19010  1stcfb  19049  1stcelcls  19065  txcnpi  19181  txcnp  19193  txtube  19213  qtoptop2  19272  fgcl  19451  filssufilg  19484  ufileu  19492  uffix  19494  elfm2  19521  fmfnfmlem1  19527  fmco  19534  fbflim2  19550  flffbas  19568  flftg  19569  cnpflf2  19573  alexsubALTlem4  19622  neibl  20076  metcnp3  20115  xlebnum  20537  lebnumii  20538  caubl  20818  caublcls  20819  bcthlem2  20836  bcthlem5  20839  ovolsslem  20967  volsuplem  21036  dyadmbllem  21079  ellimc3  21354  limciun  21369  cpnord  21409  ubthlem1  24271  occon3  24700  chsupval  24738  chsupcl  24743  chsupss  24745  spanss  24751  chsupval2  24813  stlei  25644  dmdbr5  25712  mdsl0  25714  chrelat2i  25769  chirredlem1  25794  mdsymlem5  25811  mdsymlem6  25812  gsumle  26246  gsumvsca1  26251  gsumvsca2  26252  omsmon  26711  cvmliftlem15  27187  limsucncmpi  28291  clsint2  28524  reftr  28561  fgmin  28591  filnetlem4  28602  heiborlem1  28710  heiborlem8  28717  incssnn0  29047  islssfg2  29424  hbtlem6  29485  sspwimpcf  31656  sspwimpcfVD  31657  pclssN  33538  dochexmidlem7  35111