Theorem 2iunin

Description: Rearrange indexed unions over intersection. (Contributed by NM, 18-Dec-2008)

	Ref	Expression
Assertion	2iunin	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 ( 𝐶 ∩ 𝐷 ) = ( ∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		iunin2	⊢ ∪ 𝑦 ∈ 𝐵 ( 𝐶 ∩ 𝐷 ) = ( 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷 )
2	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → ∪ 𝑦 ∈ 𝐵 ( 𝐶 ∩ 𝐷 ) = ( 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷 ) )
3	2	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 ( 𝐶 ∩ 𝐷 ) = ∪ 𝑥 ∈ 𝐴 ( 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷 )
4		iunin1	⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷 ) = ( ∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷 )
5	3 4	eqtri	⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 ( 𝐶 ∩ 𝐷 ) = ( ∪ 𝑥 ∈ 𝐴 𝐶 ∩ ∪ 𝑦 ∈ 𝐵 𝐷 )