Metamath Proof Explorer

Theorem coss1

Description: Subclass theorem for composition. (Contributed by FL, 30-Dec-2010)

Ref Expression
Assertion coss1 
|- ( A C_ B -> ( A o. C ) C_ ( B o. C ) )

Proof

Step Hyp Ref Expression
1 ssbr 
 |-  ( A C_ B -> ( y A z -> y B z ) )
2 1 anim2d 
 |-  ( A C_ B -> ( ( x C y /\ y A z ) -> ( x C y /\ y B z ) ) )
3 2 eximdv 
 |-  ( A C_ B -> ( E. y ( x C y /\ y A z ) -> E. y ( x C y /\ y B z ) ) )
4 3 ssopab2dv 
 |-  ( A C_ B -> { <. x , z >. | E. y ( x C y /\ y A z ) } C_ { <. x , z >. | E. y ( x C y /\ y B z ) } )
5 df-co 
 |-  ( A o. C ) = { <. x , z >. | E. y ( x C y /\ y A z ) }
6 df-co 
 |-  ( B o. C ) = { <. x , z >. | E. y ( x C y /\ y B z ) }
7 4 5 6 3sstr4g 
 |-  ( A C_ B -> ( A o. C ) C_ ( B o. C ) )