Metamath Proof Explorer


Theorem coss1

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

Ref Expression
Assertion coss1 ABACBC

Proof

Step Hyp Ref Expression
1 ssbr AByAzyBz
2 1 anim2d ABxCyyAzxCyyBz
3 2 eximdv AByxCyyAzyxCyyBz
4 3 ssopab2dv ABxz|yxCyyAzxz|yxCyyBz
5 df-co AC=xz|yxCyyAz
6 df-co BC=xz|yxCyyBz
7 4 5 6 3sstr4g ABACBC