Theorem iineq12dv

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

	Ref	Expression
Hypotheses	iineq12dv.1	$$⊢\phi \to A=B$$
	iineq12dv.2	$$⊢\left(\phi \wedge x\in B\right)\to C=D$$
Assertion	iineq12dv	$$⊢\phi \to \bigcap _{x\in A}C=\bigcap _{x\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		iineq12dv.1	$$⊢\phi \to A=B$$
2		iineq12dv.2	$$⊢\left(\phi \wedge x\in B\right)\to C=D$$
3	1	iineq1d	$$⊢\phi \to \bigcap _{x\in A}C=\bigcap _{x\in B}C$$
4	2	iineq2dv	$$⊢\phi \to \bigcap _{x\in B}C=\bigcap _{x\in B}D$$
5	3 4	eqtrd	$$⊢\phi \to \bigcap _{x\in A}C=\bigcap _{x\in B}D$$