Metamath Proof Explorer


Theorem coss2

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

Ref Expression
Assertion coss2 ABCACB

Proof

Step Hyp Ref Expression
1 ssbr ABxAyxBy
2 1 anim1d ABxAyyCzxByyCz
3 2 eximdv AByxAyyCzyxByyCz
4 3 ssopab2dv ABxz|yxAyyCzxz|yxByyCz
5 df-co CA=xz|yxAyyCz
6 df-co CB=xz|yxByyCz
7 4 5 6 3sstr4g ABCACB