Theorem iniin1

Description: Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	iniin1	$$⊢A\ne \varnothing \to \bigcap _{x\in A}C\cap B=\bigcap _{x\in A}\left(C\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iinin1	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(C\cap B\right)=\bigcap _{x\in A}C\cap B$$
2	1	eqcomd	$$⊢A\ne \varnothing \to \bigcap _{x\in A}C\cap B=\bigcap _{x\in A}\left(C\cap B\right)$$