resiun2

Description: Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015)

		Ref	Expression
	Assertion	resiun2	$⊢ {C ↾}_{⋃_{x \in A} B} = ⋃_{x \in A} ({C ↾}_{B})$

Step	Hyp	Ref	Expression
1		df-res	$⊢ {C ↾}_{⋃_{x \in A} B} = C \cap (⋃_{x \in A} B \times V)$
2		df-res	$⊢ {C ↾}_{B} = C \cap (B \times V)$
3	2	a1i	$⊢ x \in A \to {C ↾}_{B} = C \cap (B \times V)$
4	3	iuneq2i	$⊢ ⋃_{x \in A} ({C ↾}_{B}) = ⋃_{x \in A} (C \cap (B \times V))$
5		xpiundir	$⊢ ⋃_{x \in A} B \times V = ⋃_{x \in A} (B \times V)$
6	5	ineq2i	$⊢ C \cap (⋃_{x \in A} B \times V) = C \cap ⋃_{x \in A} (B \times V)$
7		iunin2	$⊢ ⋃_{x \in A} (C \cap (B \times V)) = C \cap ⋃_{x \in A} (B \times V)$
8	6 7	eqtr4i	$⊢ C \cap (⋃_{x \in A} B \times V) = ⋃_{x \in A} (C \cap (B \times V))$
9	4 8	eqtr4i	$⊢ ⋃_{x \in A} ({C ↾}_{B}) = C \cap (⋃_{x \in A} B \times V)$
10	1 9	eqtr4i	$⊢ {C ↾}_{⋃_{x \in A} B} = ⋃_{x \in A} ({C ↾}_{B})$

Metamath Proof Explorer