Theorem iniin2

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

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

Proof

Step	Hyp	Ref	Expression
1		iinin2	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
2	1	eqcomd	⊢ ( 𝐴 ≠ ∅ → ( 𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) )