Theorem sstr2 3360

Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-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 3347	. . . 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 1680	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3342	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3342	. 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 1362   e. wcel 1761   C_ wss 3325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3332  df-ss 3339

This theorem is referenced by:  sstr  3361  sstri  3362  sseq1  3374  sseq2  3375  ssun3  3518  ssun4  3519  ssinss1  3575  ssdisj  3725  triun  4395  trint0  4399  sspwb  4538  exss  4552  frss  4683  relss  4923  funss  5433  funimass2  5489  fss  5564  suceloni  6423  limsssuc  6460  oaordi  6981  oeworde  7028  nnaordi  7053  sbthlem2  7418  sbthlem3  7419  sbthlem6  7422  domunfican  7580  fiint  7584  fiss  7670  dffi3  7677  inf3lem1  7830  trcl  7944  tcss  7960  ac10ct  8200  ackbij2lem4  8407  cfslb  8431  cfslbn  8432  cfcoflem  8437  coftr  8438  fin23lem15  8499  fin23lem20  8502  fin23lem36  8513  isf32lem1  8518  axdc3lem2  8616  ttukeylem2  8675  wunex2  8901  tskcard  8944  mrcss  14550  isacs2  14587  lubss  15287  frmdss2  15534  lsmlub  16155  lsslss  17020  lspss  17043  aspss  17381  mplcoe1  17534  mplcoe2  17537  mplcoe2OLD  17538  ocv2ss  17998  ocvsscon  18000  lindsss  18153  lsslinds  18160  mdetunilem9  18326  tgss  18473  tgcl  18474  tgss3  18491  clsss  18558  ntrss  18559  neiss  18613  ssnei2  18620  opnnei  18624  cnpnei  18768  cnpco  18771  cncls  18778  cnprest  18793  hauscmp  18910  1stcfb  18949  1stcelcls  18965  txcnpi  19081  txcnp  19093  txtube  19113  qtoptop2  19172  fgcl  19351  filssufilg  19384  ufileu  19392  uffix  19394  elfm2  19421  fmfnfmlem1  19427  fmco  19434  fbflim2  19450  flffbas  19468  flftg  19469  cnpflf2  19473  alexsubALTlem4  19522  neibl  19976  metcnp3  20015  xlebnum  20437  lebnumii  20438  caubl  20718  caublcls  20719  bcthlem2  20736  bcthlem5  20739  ovolsslem  20867  volsuplem  20936  dyadmbllem  20979  ellimc3  21254  limciun  21269  cpnord  21309  ubthlem1  24190  occon3  24619  chsupval  24657  chsupcl  24662  chsupss  24664  spanss  24670  chsupval2  24732  stlei  25563  dmdbr5  25631  mdsl0  25633  chrelat2i  25688  chirredlem1  25713  mdsymlem5  25730  mdsymlem6  25731  gsumle  26165  gsumvsca1  26170  gsumvsca2  26171  cvmliftlem15  27101  limsucncmpi  28205  clsint2  28433  reftr  28470  fgmin  28500  filnetlem4  28511  heiborlem1  28619  heiborlem8  28626  incssnn0  28956  islssfg2  29333  hbtlem6  29394  sspwimpcf  31473  sspwimpcfVD  31474  pclssN  33226  dochexmidlem7  34799