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	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(C\cap B\right)=\bigcap _{x\in A}C\cap B$$

Proof

Step	Hyp	Ref	Expression
1		iinin2	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(B\cap C\right)=B\cap \bigcap _{x\in A}C$$
2		incom	$$⊢C\cap B=B\cap C$$
3	2	a1i	$$⊢x\in A\to C\cap B=B\cap C$$
4	3	iineq2i	$$⊢\bigcap _{x\in A}\left(C\cap B\right)=\bigcap _{x\in A}\left(B\cap C\right)$$
5		incom	$$⊢\bigcap _{x\in A}C\cap B=B\cap \bigcap _{x\in A}C$$
6	1 4 5	3eqtr4g	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(C\cap B\right)=\bigcap _{x\in A}C\cap B$$