Theorem sstr2 3511

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 3498	. . . 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 1685	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3493	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3493	. 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 1377   e. wcel 1767   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  sstr  3512  sstri  3513  sseq1  3525  sseq2  3526  ssun3  3669  ssun4  3670  ssinss1  3726  ssdisj  3876  triun  4553  trint0  4557  sspwb  4696  exss  4710  frss  4846  relss  5090  funss  5606  funimass2  5662  fss  5739  suceloni  6632  limsssuc  6669  oaordi  7195  oeworde  7242  nnaordi  7267  sbthlem2  7628  sbthlem3  7629  sbthlem6  7632  domunfican  7793  fiint  7797  fiss  7884  dffi3  7891  inf3lem1  8045  trcl  8159  tcss  8175  ac10ct  8415  ackbij2lem4  8622  cfslb  8646  cfslbn  8647  cfcoflem  8652  coftr  8653  fin23lem15  8714  fin23lem20  8717  fin23lem36  8728  isf32lem1  8733  axdc3lem2  8831  ttukeylem2  8890  wunex2  9116  tskcard  9159  mrcss  14871  isacs2  14908  lubss  15608  frmdss2  15863  lsmlub  16489  lsslss  17407  lspss  17430  aspss  17780  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  ocv2ss  18499  ocvsscon  18501  lindsss  18654  lsslinds  18661  mdetunilem9  18917  tgss  19264  tgcl  19265  tgss3  19282  clsss  19349  ntrss  19350  neiss  19404  ssnei2  19411  opnnei  19415  cnpnei  19559  cnpco  19562  cncls  19569  cnprest  19584  hauscmp  19701  1stcfb  19740  1stcelcls  19756  txcnpi  19872  txcnp  19884  txtube  19904  qtoptop2  19963  fgcl  20142  filssufilg  20175  ufileu  20183  uffix  20185  elfm2  20212  fmfnfmlem1  20218  fmco  20225  fbflim2  20241  flffbas  20259  flftg  20260  cnpflf2  20264  alexsubALTlem4  20313  neibl  20767  metcnp3  20806  xlebnum  21228  lebnumii  21229  caubl  21509  caublcls  21510  bcthlem2  21527  bcthlem5  21530  ovolsslem  21658  volsuplem  21728  dyadmbllem  21771  ellimc3  22046  limciun  22061  cpnord  22101  ubthlem1  25490  occon3  25919  chsupval  25957  chsupcl  25962  chsupss  25964  spanss  25970  chsupval2  26032  stlei  26863  dmdbr5  26931  mdsl0  26933  chrelat2i  26988  chirredlem1  27013  mdsymlem5  27030  mdsymlem6  27031  gsumle  27461  gsumvsca1  27464  gsumvsca2  27465  omsmon  27935  cvmliftlem15  28411  limsucncmpi  29515  clsint2  29752  reftr  29789  fgmin  29819  filnetlem4  29830  heiborlem1  29938  heiborlem8  29945  incssnn0  30275  islssfg2  30649  hbtlem6  30710  sspwimpcf  32818  sspwimpcfVD  32819  pclssN  34708  dochexmidlem7  36281