Theorem iineq1i

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

	Ref	Expression
Hypothesis	iineq1i.1	$$⊢A=B$$
Assertion	iineq1i	$$⊢\bigcap _{x\in A}C=\bigcap _{x\in B}C$$

Proof

Step	Hyp	Ref	Expression
1		iineq1i.1	$$⊢A=B$$
2	1	eleq2i	$$⊢x\in A\leftrightarrow x\in B$$
3	2	imbi1i	$$⊢\left(x\in A\to t\in C\right)\leftrightarrow \left(x\in B\to t\in C\right)$$
4	3	ralbii2	$$⊢\forall x\in At\in C\leftrightarrow \forall x\in Bt\in C$$
5	4	abbii	$$⊢\left\{t|\forall x\in At\in C\right\}=\left\{t|\forall x\in Bt\in C\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}C=\left\{t|\forall x\in Bt\in C\right\}$$
8	5 6 7	3eqtr4i	$$⊢\bigcap _{x\in A}C=\bigcap _{x\in B}C$$