Theorem cbviunf

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006) (Revised by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Hypotheses	cbviunf.x	$$⊢\underset{\_}{Ⅎ}xA$$
	cbviunf.y	$$⊢\underset{\_}{Ⅎ}yA$$
	cbviunf.1	$$⊢\underset{\_}{Ⅎ}yB$$
	cbviunf.2	$$⊢\underset{\_}{Ⅎ}xC$$
	cbviunf.3	$$⊢x=y\to B=C$$
Assertion	cbviunf	$$⊢\bigcup _{x\in A}B=\bigcup _{y\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		cbviunf.x	$$⊢\underset{\_}{Ⅎ}xA$$
2		cbviunf.y	$$⊢\underset{\_}{Ⅎ}yA$$
3		cbviunf.1	$$⊢\underset{\_}{Ⅎ}yB$$
4		cbviunf.2	$$⊢\underset{\_}{Ⅎ}xC$$
5		cbviunf.3	$$⊢x=y\to B=C$$
6	3	nfcri	$$⊢Ⅎyz\in B$$
7	4	nfcri	$$⊢Ⅎxz\in C$$
8	5	eleq2d	$$⊢x=y\to \left(z\in B\leftrightarrow z\in C\right)$$
9	1 2 6 7 8	cbvrexfw	$$⊢\exists x\in Az\in B\leftrightarrow \exists y\in Az\in C$$
10	9	abbii	$$⊢\left\{z|\exists x\in Az\in B\right\}=\left\{z|\exists y\in Az\in C\right\}$$
11		df-iun	$$⊢\bigcup _{x\in A}B=\left\{z|\exists x\in Az\in B\right\}$$
12		df-iun	$$⊢\bigcup _{y\in A}C=\left\{z|\exists y\in Az\in C\right\}$$
13	10 11 12	3eqtr4i	$$⊢\bigcup _{x\in A}B=\bigcup _{y\in A}C$$