Theorem sstr2 3496

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 3483	. . . 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 1714	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3478	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3478	. 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 1396   e. wcel 1823   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475

This theorem is referenced by:  sstr  3497  sstri  3498  sseq1  3510  sseq2  3511  ssun3  3655  ssun4  3656  ssinss1  3712  ssdisj  3864  triun  4545  trint0  4549  sspwb  4686  exss  4700  frss  4835  relss  5078  funss  5588  funimass2  5644  fss  5721  suceloni  6621  limsssuc  6658  oaordi  7187  oeworde  7234  nnaordi  7259  sbthlem2  7621  sbthlem3  7622  sbthlem6  7625  domunfican  7785  fiint  7789  fiss  7876  dffi3  7883  inf3lem1  8036  trcl  8150  tcss  8166  ac10ct  8406  ackbij2lem4  8613  cfslb  8637  cfslbn  8638  cfcoflem  8643  coftr  8644  fin23lem15  8705  fin23lem20  8708  fin23lem36  8719  isf32lem1  8724  axdc3lem2  8822  ttukeylem2  8881  wunex2  9105  tskcard  9148  clsslem  12902  mrcss  15105  isacs2  15142  lubss  15950  frmdss2  16230  lsmlub  16882  lsslss  17802  lspss  17825  aspss  18176  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  ocv2ss  18877  ocvsscon  18879  lindsss  19026  lsslinds  19033  mdetunilem9  19289  tgss  19637  tgcl  19638  tgss3  19655  clsss  19722  ntrss  19723  neiss  19777  ssnei2  19784  opnnei  19788  cnpnei  19932  cnpco  19935  cncls  19942  cnprest  19957  hauscmp  20074  1stcfb  20112  1stcelcls  20128  reftr  20181  txcnpi  20275  txcnp  20287  txtube  20307  qtoptop2  20366  fgcl  20545  filssufilg  20578  ufileu  20586  uffix  20588  elfm2  20615  fmfnfmlem1  20621  fmco  20628  fbflim2  20644  flffbas  20662  flftg  20663  cnpflf2  20667  alexsubALTlem4  20716  neibl  21170  metcnp3  21209  xlebnum  21631  lebnumii  21632  caubl  21912  caublcls  21913  bcthlem2  21930  bcthlem5  21933  ovolsslem  22061  volsuplem  22131  dyadmbllem  22174  ellimc3  22449  limciun  22464  cpnord  22504  ubthlem1  25984  occon3  26413  chsupval  26451  chsupcl  26456  chsupss  26458  spanss  26464  chsupval2  26526  stlei  27357  dmdbr5  27425  mdsl0  27427  chrelat2i  27482  chirredlem1  27507  mdsymlem5  27524  mdsymlem6  27525  gsumle  28004  gsumvsca1  28008  gsumvsca2  28009  omsmon  28506  cvmliftlem15  29007  ss2mcls  29192  mclsax  29193  limsucncmpi  30138  clsint2  30387  fgmin  30428  filnetlem4  30439  heiborlem1  30547  heiborlem8  30554  incssnn0  30883  islssfg2  31256  hbtlem6  31319  dvmptfprod  31981  elbigo2  33427  sspwimpcf  34121  sspwimpcfVD  34122  pclssN  36015  dochexmidlem7  37590  hess  38253  psshepw  38261