Theorem sstr2 3471

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 3458	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	imim1d 78	. . 3 |- ( A C_ B -> ( ( x e. B -> x e. C ) -> ( x e. A -> x e. C ) ) )
3	2	alimdv 1753	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3453	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3453	. 2 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6	3, 4, 5	3imtr4g 273	1 |- ( A C_ B -> ( B C_ C -> A C_ C ) )

Syntax hints:   -> wi 4   A.wal 1435   e. wcel 1868   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450

This theorem is referenced by:  sstr  3472  sstri  3473  sseq1  3485  sseq2  3486  ssun3  3631  ssun4  3632  ssinss1  3690  ssdisj  3842  triun  4528  trint0  4532  sspwb  4667  exss  4681  frss  4817  relss  4938  funss  5616  funimass2  5672  fss  5751  suceloni  6651  limsssuc  6688  oaordi  7252  oeworde  7299  nnaordi  7324  sbthlem2  7686  sbthlem3  7687  sbthlem6  7690  domunfican  7847  fiint  7851  fiss  7941  dffi3  7948  inf3lem1  8136  trcl  8214  tcss  8230  ac10ct  8466  ackbij2lem4  8673  cfslb  8697  cfslbn  8698  cfcoflem  8703  coftr  8704  fin23lem15  8765  fin23lem20  8768  fin23lem36  8779  isf32lem1  8784  axdc3lem2  8882  ttukeylem2  8941  wunex2  9164  tskcard  9207  clsslem  13037  mrcss  15510  isacs2  15547  lubss  16355  frmdss2  16635  lsmlub  17303  lsslss  18172  lspss  18195  aspss  18544  mplcoe1  18677  mplcoe5  18680  ocv2ss  19223  ocvsscon  19225  lindsss  19369  lsslinds  19376  mdetunilem9  19632  tgss  19971  tgcl  19972  tgss3  19989  clsss  20056  ntrss  20057  neiss  20112  ssnei2  20119  opnnei  20123  cnpnei  20267  cnpco  20270  cncls  20277  cnprest  20292  hauscmp  20409  1stcfb  20447  1stcelcls  20463  reftr  20516  txcnpi  20610  txcnp  20622  txtube  20642  qtoptop2  20701  fgcl  20880  filssufilg  20913  ufileu  20921  uffix  20923  elfm2  20950  fmfnfmlem1  20956  fmco  20963  fbflim2  20979  flffbas  20997  flftg  20998  cnpflf2  21002  alexsubALTlem4  21052  neibl  21503  metcnp3  21542  xlebnum  21983  lebnumii  21984  caubl  22264  caublcls  22265  bcthlem2  22280  bcthlem5  22283  ovolsslem  22424  volsuplem  22495  dyadmbllem  22544  ellimc3  22821  limciun  22836  cpnord  22876  ubthlem1  26498  occon3  26936  chsupval  26974  chsupcl  26979  chsupss  26981  spanss  26987  chsupval2  27049  stlei  27879  dmdbr5  27947  mdsl0  27949  chrelat2i  28004  chirredlem1  28029  mdsymlem5  28046  mdsymlem6  28047  gsumle  28537  gsumvsca1  28541  gsumvsca2  28542  omsmon  29122  omsmonOLD  29126  cvmliftlem15  30017  ss2mcls  30202  mclsax  30203  clsint2  30978  fgmin  31019  filnetlem4  31030  limsucncmpi  31098  ptrecube  31854  heiborlem1  32057  heiborlem8  32064  pclssN  33378  dochexmidlem7  34953  incssnn0  35472  islssfg2  35849  hbtlem6  35908  hess  36233  psshepw  36242  sspwimpcf  37178  sspwimpcfVD  37179  dvmptfprod  37640  elbigo2  39637