Theorem iinun2

Description: Indexed intersection of union. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004)

	Ref	Expression
Assertion	iinun2	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) = ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		r19.32v	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
2		elun	⊢ ( 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶 ) )
4		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
5	4	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
6	5	orbi2i	⊢ ( ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) )
7	1 3 6	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
8		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) ) )
9	8	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( 𝐵 ∪ 𝐶 ) )
10		elun	⊢ ( 𝑦 ∈ ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∨ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
11	7 9 10	3bitr4i	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) ↔ 𝑦 ∈ ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
12	11	eqriv	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∪ 𝐶 ) = ( 𝐵 ∪ ∩ 𝑥 ∈ 𝐴 𝐶 )