resres

Description: The restriction of a restriction. (Contributed by NM, 27-Mar-2008)

		Ref	Expression
	Assertion	resres	$⊢ {({A ↾}_{B}) ↾}_{C} = {A ↾}_{(B \cap C)}$

Step	Hyp	Ref	Expression
1		df-res	$⊢ {({A ↾}_{B}) ↾}_{C} = ({A ↾}_{B}) \cap (C \times V)$
2		df-res	$⊢ {A ↾}_{B} = A \cap (B \times V)$
3	2	ineq1i	$⊢ ({A ↾}_{B}) \cap (C \times V) = (A \cap (B \times V)) \cap (C \times V)$
4		xpindir	$⊢ (B \cap C) \times V = (B \times V) \cap (C \times V)$
5	4	ineq2i	$⊢ A \cap ((B \cap C) \times V) = A \cap ((B \times V) \cap (C \times V))$
6		df-res	$⊢ {A ↾}_{(B \cap C)} = A \cap ((B \cap C) \times V)$
7		inass	$⊢ (A \cap (B \times V)) \cap (C \times V) = A \cap ((B \times V) \cap (C \times V))$
8	5 6 7	3eqtr4ri	$⊢ (A \cap (B \times V)) \cap (C \times V) = {A ↾}_{(B \cap C)}$
9	1 3 8	3eqtri	$⊢ {({A ↾}_{B}) ↾}_{C} = {A ↾}_{(B \cap C)}$

Metamath Proof Explorer