Theorem sstr2 3208

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 3195	. . . 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 1903	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		ssalel 3189	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		ssalel 3189	. 2 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6	3, 4, 5	3imtr4g 205	1 |- ( A C_ B -> ( B C_ C -> A C_ C ) )

Syntax hints:   -> wi 4   A.wal 1371   e. wcel 2178   C_ wss 3174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  sstr  3209  sstri  3210  sseq1  3224  sseq2  3225  ssun3  3346  ssun4  3347  ssinss1  3410  ssdisj  3525  triun  4171  trintssm  4174  sspwb  4278  exss  4289  relss  4780  funss  5309  funimass2  5371  fss  5457  fiintim  7054  sbthlem2  7086  sbthlemi3  7087  sbthlemi6  7090  lsslss  14258  lspss  14276  tgss  14650  tgcl  14651  tgss3  14665  clsss  14705  neiss  14737  ssnei2  14744  cnpnei  14806  cnptopco  14809  cnptoprest  14826  txcnp  14858  neibl  15078  metcnp3  15098  bj-nntrans  16086