Theorem sstr2 3493

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 3480	. . . 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 1694	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3475	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3475	. 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 1379   e. wcel 1802   C_ wss 3458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472

This theorem is referenced by:  sstr  3494  sstri  3495  sseq1  3507  sseq2  3508  ssun3  3651  ssun4  3652  ssinss1  3708  ssdisj  3858  triun  4539  trint0  4543  sspwb  4682  exss  4696  frss  4832  relss  5076  funss  5592  funimass2  5648  fss  5725  suceloni  6629  limsssuc  6666  oaordi  7193  oeworde  7240  nnaordi  7265  sbthlem2  7626  sbthlem3  7627  sbthlem6  7630  domunfican  7791  fiint  7795  fiss  7882  dffi3  7889  inf3lem1  8043  trcl  8157  tcss  8173  ac10ct  8413  ackbij2lem4  8620  cfslb  8644  cfslbn  8645  cfcoflem  8650  coftr  8651  fin23lem15  8712  fin23lem20  8715  fin23lem36  8726  isf32lem1  8731  axdc3lem2  8829  ttukeylem2  8888  wunex2  9114  tskcard  9157  mrcss  14885  isacs2  14922  lubss  15620  frmdss2  15900  lsmlub  16552  lsslss  17475  lspss  17498  aspss  17849  mplcoe1  17995  mplcoe5  17999  mplcoe2OLD  18001  ocv2ss  18571  ocvsscon  18573  lindsss  18726  lsslinds  18733  mdetunilem9  18989  tgss  19336  tgcl  19337  tgss3  19354  clsss  19421  ntrss  19422  neiss  19476  ssnei2  19483  opnnei  19487  cnpnei  19631  cnpco  19634  cncls  19641  cnprest  19656  hauscmp  19773  1stcfb  19812  1stcelcls  19828  reftr  19881  txcnpi  19975  txcnp  19987  txtube  20007  qtoptop2  20066  fgcl  20245  filssufilg  20278  ufileu  20286  uffix  20288  elfm2  20315  fmfnfmlem1  20321  fmco  20328  fbflim2  20344  flffbas  20362  flftg  20363  cnpflf2  20367  alexsubALTlem4  20416  neibl  20870  metcnp3  20909  xlebnum  21331  lebnumii  21332  caubl  21612  caublcls  21613  bcthlem2  21630  bcthlem5  21633  ovolsslem  21761  volsuplem  21831  dyadmbllem  21874  ellimc3  22149  limciun  22164  cpnord  22204  ubthlem1  25651  occon3  26080  chsupval  26118  chsupcl  26123  chsupss  26125  spanss  26131  chsupval2  26193  stlei  27024  dmdbr5  27092  mdsl0  27094  chrelat2i  27149  chirredlem1  27174  mdsymlem5  27191  mdsymlem6  27192  gsumle  27636  gsumvsca1  27639  gsumvsca2  27640  omsmon  28133  cvmliftlem15  28609  ss2mcls  28794  mclsax  28795  limsucncmpi  29878  clsint2  30115  fgmin  30156  filnetlem4  30167  heiborlem1  30275  heiborlem8  30282  incssnn0  30611  islssfg2  30985  hbtlem6  31046  sspwimpcf  33428  sspwimpcfVD  33429  pclssN  35320  dochexmidlem7  36895