Theorem coss1

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

	Ref	Expression
Assertion	coss1	$$⊢A\subseteq B\to A\circ C\subseteq B\circ C$$

Proof

Step	Hyp	Ref	Expression
1		ssbr	$$⊢A\subseteq B\to \left(yAz\to yBz\right)$$
2	1	anim2d	$$⊢A\subseteq B\to \left(\left(xCy\wedge yAz\right)\to \left(xCy\wedge yBz\right)\right)$$
3	2	eximdv	$$⊢A\subseteq B\to \left(\exists y\left(xCy\wedge yAz\right)\to \exists y\left(xCy\wedge yBz\right)\right)$$
4	3	ssopab2dv	$$⊢A\subseteq B\to \left\{⟨x,z⟩|\exists y\left(xCy\wedge yAz\right)\right\}\subseteq \left\{⟨x,z⟩|\exists y\left(xCy\wedge yBz\right)\right\}$$
5		df-co	$$⊢A\circ C=\left\{⟨x,z⟩|\exists y\left(xCy\wedge yAz\right)\right\}$$
6		df-co	$$⊢B\circ C=\left\{⟨x,z⟩|\exists y\left(xCy\wedge yBz\right)\right\}$$
7	4 5 6	3sstr4g	$$⊢A\subseteq B\to A\circ C\subseteq B\circ C$$