Theorem sstr2 3451

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 3438	. . . 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 1774	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3433	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3433	. 2 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6	3, 4, 5	3imtr4g 278	1 |- ( A C_ B -> ( B C_ C -> A C_ C ) )

Syntax hints:   -> wi 4   A.wal 1453   e. wcel 1898   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430

This theorem is referenced by:  sstr  3452  sstri  3453  sseq1  3465  sseq2  3466  ssun3  3611  ssun4  3612  ssinss1  3672  ssdisj  3826  triun  4524  trint0  4528  sspwb  4663  exss  4677  frss  4820  relss  4941  funss  5619  funimass2  5679  fss  5760  suceloni  6667  limsssuc  6704  oaordi  7273  oeworde  7320  nnaordi  7345  sbthlem2  7709  sbthlem3  7710  sbthlem6  7713  domunfican  7870  fiint  7874  fiss  7964  dffi3  7971  inf3lem1  8159  trcl  8238  tcss  8254  ac10ct  8491  ackbij2lem4  8698  cfslb  8722  cfslbn  8723  cfcoflem  8728  coftr  8729  fin23lem15  8790  fin23lem20  8793  fin23lem36  8804  isf32lem1  8809  axdc3lem2  8907  ttukeylem2  8966  wunex2  9189  tskcard  9232  clsslem  13097  mrcss  15571  isacs2  15608  lubss  16416  frmdss2  16696  lsmlub  17364  lsslss  18233  lspss  18256  aspss  18605  mplcoe1  18738  mplcoe5  18741  ocv2ss  19285  ocvsscon  19287  lindsss  19431  lsslinds  19438  mdetunilem9  19694  tgss  20033  tgcl  20034  tgss3  20051  clsss  20118  ntrss  20119  neiss  20174  ssnei2  20181  opnnei  20185  cnpnei  20329  cnpco  20332  cncls  20339  cnprest  20354  hauscmp  20471  1stcfb  20509  1stcelcls  20525  reftr  20578  txcnpi  20672  txcnp  20684  txtube  20704  qtoptop2  20763  fgcl  20942  filssufilg  20975  ufileu  20983  uffix  20985  elfm2  21012  fmfnfmlem1  21018  fmco  21025  fbflim2  21041  flffbas  21059  flftg  21060  cnpflf2  21064  alexsubALTlem4  21114  neibl  21565  metcnp3  21604  xlebnum  22045  lebnumii  22046  caubl  22326  caublcls  22327  bcthlem2  22342  bcthlem5  22345  ovolsslem  22486  volsuplem  22557  dyadmbllem  22606  ellimc3  22883  limciun  22898  cpnord  22938  ubthlem1  26561  occon3  26999  chsupval  27037  chsupcl  27042  chsupss  27044  spanss  27050  chsupval2  27112  stlei  27942  dmdbr5  28010  mdsl0  28012  chrelat2i  28067  chirredlem1  28092  mdsymlem5  28109  mdsymlem6  28110  gsumle  28591  gsumvsca1  28594  gsumvsca2  28595  omsmon  29175  omsmonOLD  29179  cvmliftlem15  30070  ss2mcls  30255  mclsax  30256  clsint2  31034  fgmin  31075  filnetlem4  31086  limsucncmpi  31154  ptrecube  31985  heiborlem1  32188  heiborlem8  32195  pclssN  33504  dochexmidlem7  35079  incssnn0  35598  islssfg2  35974  hbtlem6  36033  hess  36420  psshepw  36429  sspwimpcf  37357  sspwimpcfVD  37358  dvmptfprod  37858  elbigo2  40636