Theorem iineq1

Description: Equality theorem for indexed intersection. (Contributed by NM, 27-Jun-1998)

	Ref	Expression
Assertion	iineq1	$$⊢A=B\to \bigcap _{x\in A}C=\bigcap _{x\in B}C$$

Proof

Step	Hyp	Ref	Expression
1		raleq	$$⊢A=B\to \left(\forall x\in Ay\in C\leftrightarrow \forall x\in By\in C\right)$$
2	1	abbidv	$$⊢A=B\to \left\{y|\forall x\in Ay\in C\right\}=\left\{y|\forall x\in By\in C\right\}$$
3		df-iin	$$⊢\bigcap _{x\in A}C=\left\{y|\forall x\in Ay\in C\right\}$$
4		df-iin	$$⊢\bigcap _{x\in B}C=\left\{y|\forall x\in By\in C\right\}$$
5	2 3 4	3eqtr4g	$$⊢A=B\to \bigcap _{x\in A}C=\bigcap _{x\in B}C$$