Theorem cbviun

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) Add disjoint variable condition to avoid ax-13 . See cbviung for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

	Ref	Expression
Hypotheses	cbviun.1	$$⊢\underset{\_}{Ⅎ}yB$$
	cbviun.2	$$⊢\underset{\_}{Ⅎ}xC$$
	cbviun.3	$$⊢x=y\to B=C$$
Assertion	cbviun	$$⊢\bigcup _{x\in A}B=\bigcup _{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	cbvrexw	$$⊢\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$$