Theorem sstr2 3235

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 3222	. . . 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 1927	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		ssalel 3216	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		ssalel 3216	. 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 1396   e. wcel 2202   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sstr  3236  sstri  3237  sseq1  3251  sseq2  3252  ssun3  3374  ssun4  3375  ssinss1  3438  ssdisj  3553  triun  4205  trintssm  4208  sspwb  4314  exss  4325  relss  4819  funss  5352  funimass2  5415  fss  5501  fiintim  7166  sbthlem2  7200  sbthlemi3  7201  sbthlemi6  7204  lsslss  14460  lspss  14478  tgss  14857  tgcl  14858  tgss3  14872  clsss  14912  neiss  14944  ssnei2  14951  cnpnei  15013  cnptopco  15016  cnptoprest  15033  txcnp  15065  neibl  15285  metcnp3  15305  bj-nntrans  16650