Theorem cbviin

Description: Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009) (Revised by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See cbviing for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024)

	Ref	Expression
Hypotheses	cbviun.1	$$⊢\underset{\_}{Ⅎ}yB$$
	cbviun.2	$$⊢\underset{\_}{Ⅎ}xC$$
	cbviun.3	$$⊢x=y\to B=C$$
Assertion	cbviin	$$⊢\bigcap _{x\in A}B=\bigcap _{y\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		cbviun.1	$$⊢\underset{\_}{Ⅎ}yB$$
2		cbviun.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		cbviun.3	$$⊢x=y\to B=C$$
4	1	nfcri	$$⊢Ⅎyz\in B$$
5	2	nfcri	$$⊢Ⅎxz\in C$$
6	3	eleq2d	$$⊢x=y\to \left(z\in B\leftrightarrow z\in C\right)$$
7	4 5 6	cbvralw	$$⊢\forall x\in Az\in B\leftrightarrow \forall y\in Az\in C$$
8	7	abbii	$$⊢\left\{z|\forall x\in Az\in B\right\}=\left\{z|\forall y\in Az\in C\right\}$$
9		df-iin	$$⊢\bigcap _{x\in A}B=\left\{z|\forall x\in Az\in B\right\}$$
10		df-iin	$$⊢\bigcap _{y\in A}C=\left\{z|\forall y\in Az\in C\right\}$$
11	8 9 10	3eqtr4i	$$⊢\bigcap _{x\in A}B=\bigcap _{y\in A}C$$