Metamath Proof Explorer

Theorem sstr2

Description: Transitivity of subclass relationship. Exercise 5 of TakeutiZaring p. 17. (Contributed by NM, 24-Jun-1993) (Proof shortened by Andrew Salmon, 14-Jun-2011) Avoid axioms. (Revised by GG, 19-May-2025)

Ref Expression
Assertion sstr2 
|- ( A C_ B -> ( B C_ C -> A C_ C ) )

Proof

Step Hyp Ref Expression
1 imim1 
 |-  ( ( x e. A -> x e. B ) -> ( ( x e. B -> x e. C ) -> ( x e. A -> x e. C ) ) )
2 1 al2imi 
 |-  ( A. x ( x e. A -> x e. B ) -> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
3 df-ss 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4 df-ss 
 |-  ( B C_ C <-> A. x ( x e. B -> x e. C ) )
5 df-ss 
 |-  ( A C_ C <-> A. x ( x e. A -> x e. C ) )
6 4 5 imbi12i 
 |-  ( ( B C_ C -> A C_ C ) <-> ( A. x ( x e. B -> x e. C ) -> A. x ( x e. A -> x e. C ) ) )
7 2 3 6 3imtr4i 
 |-  ( A C_ B -> ( B C_ C -> A C_ C ) )