This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↾}_{A} \subseteq {C ↾}_{B}$

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