Theorem cbviung

Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. Usage of this theorem is discouraged because it depends on ax-13 . See cbviun for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 26-Mar-2006) (Revised by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbviung.1	$$⊢\underset{\_}{Ⅎ}yB$$
	cbviung.2	$$⊢\underset{\_}{Ⅎ}xC$$
	cbviung.3	$$⊢x=y\to B=C$$
Assertion	cbviung	$$⊢\bigcup _{x\in A}B=\bigcup _{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	cbvrex	$$⊢\exists x\in Az\in B\leftrightarrow \exists y\in Az\in C$$
8	7	abbii	$$⊢\left\{z|\exists x\in Az\in B\right\}=\left\{z|\exists y\in Az\in C\right\}$$
9		df-iun	$$⊢\bigcup _{x\in A}B=\left\{z|\exists x\in Az\in B\right\}$$
10		df-iun	$$⊢\bigcup _{y\in A}C=\left\{z|\exists y\in Az\in C\right\}$$
11	8 9 10	3eqtr4i	$$⊢\bigcup _{x\in A}B=\bigcup _{y\in A}C$$