Theorem ssres2

Description: Subclass theorem for restriction. (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	ssres2	$$⊢A\subseteq B\to {C\upharpoonright }_A\subseteq {C\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		xpss1	$$⊢A\subseteq B\to A\times \mathrm{V}\subseteq B\times \mathrm{V}$$
2		sslin	$$⊢A\times \mathrm{V}\subseteq B\times \mathrm{V}\to C\cap \left(A\times \mathrm{V}\right)\subseteq C\cap \left(B\times \mathrm{V}\right)$$
3	1 2	syl	$$⊢A\subseteq B\to C\cap \left(A\times \mathrm{V}\right)\subseteq C\cap \left(B\times \mathrm{V}\right)$$
4		df-res	$$⊢{C\upharpoonright }_A=C\cap \left(A\times \mathrm{V}\right)$$
5		df-res	$$⊢{C\upharpoonright }_B=C\cap \left(B\times \mathrm{V}\right)$$
6	3 4 5	3sstr4g	$$⊢A\subseteq B\to {C\upharpoonright }_A\subseteq {C\upharpoonright }_B$$