Theorem sstr2 3054

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 3041	. . . 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 1818	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		dfss2 3036	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		dfss2 3036	. 2 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6	3, 4, 5	3imtr4g 204	1 |- ( A C_ B -> ( B C_ C -> A C_ C ) )

Syntax hints:   -> wi 4   A.wal 1297   e. wcel 1448   C_ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034

This theorem is referenced by:  sstr  3055  sstri  3056  sseq1  3070  sseq2  3071  ssun3  3188  ssun4  3189  ssinss1  3252  ssdisj  3366  triun  3979  trintssm  3982  sspwb  4076  exss  4087  relss  4564  funss  5078  funimass2  5137  fss  5220  fiintim  6746  sbthlem2  6774  sbthlemi3  6775  sbthlemi6  6778  tgss  12014  tgcl  12015  tgss3  12029  clsss  12069  neiss  12101  ssnei2  12108  cnpnei  12169  cnptopco  12172  cnptoprest  12189  txcnp  12221  neibl  12419  metcnp3  12435  bj-nntrans  12734