Theorem iineq12dv

Description: Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	iineq12dv.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	iineq12dv.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 = 𝐷 )
Assertion	iineq12dv	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		iineq12dv.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		iineq12dv.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 = 𝐷 )
3	1	iineq1d	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶 )
4	2	iineq2dv	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐵 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 )
5	3 4	eqtrd	⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 )