Theorem resiun2

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

	Ref	Expression
Assertion	resiun2	$$⊢{C\upharpoonright }_{\bigcup _{x\in A}B}=\bigcup _{x\in A}\left({C\upharpoonright }_B\right)$$

Proof

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