Theorem sstr2 3199

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 3186	. . . 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 1901	. 2 |- ( A C_ B -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
4		ssalel 3180	. 2 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5		ssalel 3180	. 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 1370   e. wcel 2175   C_ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  sstr  3200  sstri  3201  sseq1  3215  sseq2  3216  ssun3  3337  ssun4  3338  ssinss1  3401  ssdisj  3516  triun  4154  trintssm  4157  sspwb  4259  exss  4270  relss  4761  funss  5289  funimass2  5351  fss  5436  fiintim  7027  sbthlem2  7059  sbthlemi3  7060  sbthlemi6  7063  lsslss  14114  lspss  14132  tgss  14506  tgcl  14507  tgss3  14521  clsss  14561  neiss  14593  ssnei2  14600  cnpnei  14662  cnptopco  14665  cnptoprest  14682  txcnp  14714  neibl  14934  metcnp3  14954  bj-nntrans  15849