Theorem cbviuneq12dv

Description: Rule used to change the bound variables and classes in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by RP, 17-Jul-2020)

	Ref	Expression
Hypotheses	cbviuneq12dv.xel	$$⊢\left(\phi \wedge y\in C\right)\to X\in A$$
	cbviuneq12dv.yel	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
	cbviuneq12dv.xsub	$$⊢\left(\phi \wedge y\in C\wedge x=X\right)\to B=F$$
	cbviuneq12dv.ysub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
	cbviuneq12dv.eq1	$$⊢\left(\phi \wedge x\in A\right)\to B=G$$
	cbviuneq12dv.eq2	$$⊢\left(\phi \wedge y\in C\right)\to D=F$$
Assertion	cbviuneq12dv	$$⊢\phi \to \bigcup _{x\in A}B=\bigcup _{y\in C}D$$

Proof

Step	Hyp	Ref	Expression
1		cbviuneq12dv.xel	$$⊢\left(\phi \wedge y\in C\right)\to X\in A$$
2		cbviuneq12dv.yel	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
3		cbviuneq12dv.xsub	$$⊢\left(\phi \wedge y\in C\wedge x=X\right)\to B=F$$
4		cbviuneq12dv.ysub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
5		cbviuneq12dv.eq1	$$⊢\left(\phi \wedge x\in A\right)\to B=G$$
6		cbviuneq12dv.eq2	$$⊢\left(\phi \wedge y\in C\right)\to D=F$$
7		nfv	$$⊢Ⅎx\phi$$
8		nfv	$$⊢Ⅎy\phi$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xX$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yY$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}yC$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}xF$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}yG$$
19	7 8 9 10 11 12 13 14 15 16 17 18 1 2 3 4 5 6	cbviuneq12df	$$⊢\phi \to \bigcup _{x\in A}B=\bigcup _{y\in C}D$$