Theorem resiun1

Description: Distribution of restriction over indexed union. (Contributed by Mario Carneiro, 29-May-2015) (Proof shortened by JJ, 25-Aug-2021)

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

Proof

Step	Hyp	Ref	Expression
1		iunin1	$$⊢\bigcup _{x\in A}\left(B\cap \left(C\times \mathrm{V}\right)\right)=\bigcup _{x\in A}B\cap \left(C\times \mathrm{V}\right)$$
2		df-res	$$⊢{B\upharpoonright }_C=B\cap \left(C\times \mathrm{V}\right)$$
3	2	a1i	$$⊢x\in A\to {B\upharpoonright }_C=B\cap \left(C\times \mathrm{V}\right)$$
4	3	iuneq2i	$$⊢\bigcup _{x\in A}\left({B\upharpoonright }_C\right)=\bigcup _{x\in A}\left(B\cap \left(C\times \mathrm{V}\right)\right)$$
5		df-res	$$⊢{\bigcup _{x\in A}B\upharpoonright }_C=\bigcup _{x\in A}B\cap \left(C\times \mathrm{V}\right)$$
6	1 4 5	3eqtr4ri	$$⊢{\bigcup _{x\in A}B\upharpoonright }_C=\bigcup _{x\in A}\left({B\upharpoonright }_C\right)$$