Theorem iinin1

Description: Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Assertion	iinin1	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐶 ∩ 𝐵 ) = ( ∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		iinin2	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
2		incom	⊢ ( 𝐶 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐶 )
3	2	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐶 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐶 ) )
4	3	iineq2i	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝐶 ∩ 𝐵 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 )
5		incom	⊢ ( ∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 )
6	1 4 5	3eqtr4g	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐶 ∩ 𝐵 ) = ( ∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵 ) )