Description: Subclass theorem for composition. (Contributed by FL, 30-Dec-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | coss1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssbr | |
|
2 | 1 | anim2d | |
3 | 2 | eximdv | |
4 | 3 | ssopab2dv | |
5 | df-co | |
|
6 | df-co | |
|
7 | 4 5 6 | 3sstr4g | |