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	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↾ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		iunin1	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ ( 𝐶 × V ) )
2		df-res	⊢ ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) )
3	2	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) ) )
4	3	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↾ 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ ( 𝐶 × V ) )
5		df-res	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ ( 𝐶 × V ) )
6	1 4 5	3eqtr4ri	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↾ 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↾ 𝐶 )