Theorem cbviing

Description: Change bound variables in an indexed intersection. Usage of this theorem is discouraged because it depends on ax-13 . See cbviin for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by Jeff Hankins, 26-Aug-2009) (Revised by Mario Carneiro, 14-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbviung.1	$$⊢\underset{\_}{Ⅎ}yB$$
2		cbviung.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		cbviung.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	cbvral	$$⊢\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$$