Theorem iineq12i

Description: Equality theorem for indexed intersection. Inference version. General version of iineq1i . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	iineq12i.1	$$⊢A=B$$
	iineq12i.2	$$⊢C=D$$
Assertion	iineq12i	$$⊢\bigcap _{x\in A}C=\bigcap _{x\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		iineq12i.1	$$⊢A=B$$
2		iineq12i.2	$$⊢C=D$$
3	2	eleq2i	$$⊢t\in C\leftrightarrow t\in D$$
4	1 3	raleqbii	$$⊢\forall x\in At\in C\leftrightarrow \forall x\in Bt\in D$$
5	4	abbii	$$⊢\left\{t|\forall x\in At\in C\right\}=\left\{t|\forall x\in Bt\in D\right\}$$
6		df-iin	$$⊢\bigcap _{x\in A}C=\left\{t|\forall x\in At\in C\right\}$$
7		df-iin	$$⊢\bigcap _{x\in B}D=\left\{t|\forall x\in Bt\in D\right\}$$
8	5 6 7	3eqtr4i	$$⊢\bigcap _{x\in A}C=\bigcap _{x\in B}D$$