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(xAy\to xBy\right)$$
2	1	anim1d	$$⊢A\subseteq B\to \left(\left(xAy\wedge yCz\right)\to \left(xBy\wedge yCz\right)\right)$$
3	2	eximdv	$$⊢A\subseteq B\to \left(\exists y\left(xAy\wedge yCz\right)\to \exists y\left(xBy\wedge yCz\right)\right)$$
4	3	ssopab2dv	$$⊢A\subseteq B\to \left\{⟨x,z⟩|\exists y\left(xAy\wedge yCz\right)\right\}\subseteq \left\{⟨x,z⟩|\exists y\left(xBy\wedge yCz\right)\right\}$$
5		df-co	$$⊢C\circ A=\left\{⟨x,z⟩|\exists y\left(xAy\wedge yCz\right)\right\}$$
6		df-co	$$⊢C\circ B=\left\{⟨x,z⟩|\exists y\left(xBy\wedge yCz\right)\right\}$$
7	4 5 6	3sstr4g	$$⊢A\subseteq B\to C\circ A\subseteq C\circ B$$