Theorem sstr2 3610

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 3597	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	imim1d 82	. . 3 |- ( A C_ B -> ( ( x e. B -> x e. C ) -> ( x e. A -> x e. C ) ) )
3	2	alimdv 1845	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3591	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3591	. 2 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6	3, 4, 5	3imtr4g 285	1 |- ( A C_ B -> ( B C_ C -> A C_ C ) )

Syntax hints:   -> wi 4   A.wal 1481   e. wcel 1990   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sstr  3611  sstri  3612  sseq1  3626  sseq2  3627  ssun3  3778  ssun4  3779  ssinss1  3841  ssdisjOLD  4027  triun  4766  trintss  4769  sspwb  4917  exss  4931  frss  5081  relss  5206  funss  5907  funimass2  5972  fss  6056  suceloni  7013  limsssuc  7050  oaordi  7626  oeworde  7673  nnaordi  7698  sbthlem2  8071  sbthlem3  8072  sbthlem6  8075  domunfican  8233  fiint  8237  fiss  8330  dffi3  8337  inf3lem1  8525  trcl  8604  tcss  8620  ac10ct  8857  ackbij2lem4  9064  cfslb  9088  cfslbn  9089  cfcoflem  9094  coftr  9095  fin23lem15  9156  fin23lem20  9159  fin23lem36  9170  isf32lem1  9175  axdc3lem2  9273  ttukeylem2  9332  wunex2  9560  tskcard  9603  clsslem  13723  mrcss  16276  isacs2  16314  lubss  17121  frmdss2  17400  lsmlub  18078  lsslss  18961  lspss  18984  aspss  19332  mplcoe1  19465  mplcoe5  19468  ocv2ss  20017  ocvsscon  20019  lindsss  20163  lsslinds  20170  mdetunilem9  20426  tgss  20772  tgcl  20773  tgss3  20790  clsss  20858  ntrss  20859  neiss  20913  ssnei2  20920  opnnei  20924  cnpnei  21068  cnpco  21071  cncls  21078  cnprest  21093  hauscmp  21210  1stcfb  21248  1stcelcls  21264  reftr  21317  txcnpi  21411  txcnp  21423  txtube  21443  qtoptop2  21502  fgcl  21682  filssufilg  21715  ufileu  21723  uffix  21725  elfm2  21752  fmfnfmlem1  21758  fmco  21765  fbflim2  21781  flffbas  21799  flftg  21800  cnpflf2  21804  alexsubALTlem4  21854  neibl  22306  metcnp3  22345  xlebnum  22764  lebnumii  22765  caubl  23106  caublcls  23107  bcthlem2  23122  bcthlem5  23125  ovolsslem  23252  volsuplem  23323  dyadmbllem  23367  ellimc3  23643  limciun  23658  cpnord  23698  ubthlem1  27726  occon3  28156  chsupval  28194  chsupcl  28199  chsupss  28201  spanss  28207  chsupval2  28269  stlei  29099  dmdbr5  29167  mdsl0  29169  chrelat2i  29224  chirredlem1  29249  mdsymlem5  29266  mdsymlem6  29267  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  omsmon  30360  cvmliftlem15  31280  ss2mcls  31465  mclsax  31466  clsint2  32324  fgmin  32365  filnetlem4  32376  limsucncmpi  32444  bj-restpw  33045  bj-0int  33055  ptrecube  33409  heiborlem1  33610  heiborlem8  33617  pclssN  35180  dochexmidlem7  36755  incssnn0  37274  islssfg2  37641  hbtlem6  37699  hess  38074  psshepw  38082  clsf2  38424  sspwimpcf  39156  sspwimpcfVD  39157  dvmptfprod  40160  sprsymrelfo  41747  elbigo2  42346  setrec1lem2  42435  setrec1lem4  42437