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

Metamath Proof Explorer

Theorem ssres

Description: Subclass theorem for restriction. (Contributed by NM, 16-Aug-1994)

		Ref	Expression
	Assertion	ssres	$⊢ A \subseteq B \to {A ↾}_{C} \subseteq {B ↾}_{C}$

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