resindi

Description: Class restriction distributes over intersection. (Contributed by FL, 6-Oct-2008)

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

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

Metamath Proof Explorer