# Metamath Proof Explorer

## Theorem coss2

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

Ref Expression
Assertion coss2 ${⊢}{A}\subseteq {B}\to {C}\circ {A}\subseteq {C}\circ {B}$

### Proof

Step Hyp Ref Expression
1 ssbr ${⊢}{A}\subseteq {B}\to \left({x}{A}{y}\to {x}{B}{y}\right)$
2 1 anim1d ${⊢}{A}\subseteq {B}\to \left(\left({x}{A}{y}\wedge {y}{C}{z}\right)\to \left({x}{B}{y}\wedge {y}{C}{z}\right)\right)$
3 2 eximdv ${⊢}{A}\subseteq {B}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\wedge {y}{C}{z}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}{B}{y}\wedge {y}{C}{z}\right)\right)$
4 3 ssopab2dv ${⊢}{A}\subseteq {B}\to \left\{⟨{x},{z}⟩|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\wedge {y}{C}{z}\right)\right\}\subseteq \left\{⟨{x},{z}⟩|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}{B}{y}\wedge {y}{C}{z}\right)\right\}$
5 df-co ${⊢}{C}\circ {A}=\left\{⟨{x},{z}⟩|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}{A}{y}\wedge {y}{C}{z}\right)\right\}$
6 df-co ${⊢}{C}\circ {B}=\left\{⟨{x},{z}⟩|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}{B}{y}\wedge {y}{C}{z}\right)\right\}$
7 4 5 6 3sstr4g ${⊢}{A}\subseteq {B}\to {C}\circ {A}\subseteq {C}\circ {B}$