Metamath Proof Explorer

Theorem coss2

Description: Subclass theorem for composition. (Contributed by NM, 5-Apr-2013)

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

Proof

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