Theorem cbviuneq12df

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	cbviuneq12df.xph	$$⊢Ⅎx\phi$$
	cbviuneq12df.yph	$$⊢Ⅎy\phi$$
	cbviuneq12df.x	$$⊢\underset{\_}{Ⅎ}xX$$
	cbviuneq12df.y	$$⊢\underset{\_}{Ⅎ}yY$$
	cbviuneq12df.xa	$$⊢\underset{\_}{Ⅎ}xA$$
	cbviuneq12df.ya	$$⊢\underset{\_}{Ⅎ}yA$$
	cbviuneq12df.b	$$⊢\underset{\_}{Ⅎ}yB$$
	cbviuneq12df.xc	$$⊢\underset{\_}{Ⅎ}xC$$
	cbviuneq12df.yc	$$⊢\underset{\_}{Ⅎ}yC$$
	cbviuneq12df.d	$$⊢\underset{\_}{Ⅎ}xD$$
	cbviuneq12df.f	$$⊢\underset{\_}{Ⅎ}xF$$
	cbviuneq12df.g	$$⊢\underset{\_}{Ⅎ}yG$$
	cbviuneq12df.xel	$$⊢\left(\phi \wedge y\in C\right)\to X\in A$$
	cbviuneq12df.yel	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
	cbviuneq12df.xsub	$$⊢\left(\phi \wedge y\in C\wedge x=X\right)\to B=F$$
	cbviuneq12df.ysub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
	cbviuneq12df.eq1	$$⊢\left(\phi \wedge x\in A\right)\to B=G$$
	cbviuneq12df.eq2	$$⊢\left(\phi \wedge y\in C\right)\to D=F$$
Assertion	cbviuneq12df	$$⊢\phi \to \bigcup _{x\in A}B=\bigcup _{y\in C}D$$

Proof

Step	Hyp	Ref	Expression
1		cbviuneq12df.xph	$$⊢Ⅎx\phi$$
2		cbviuneq12df.yph	$$⊢Ⅎy\phi$$
3		cbviuneq12df.x	$$⊢\underset{\_}{Ⅎ}xX$$
4		cbviuneq12df.y	$$⊢\underset{\_}{Ⅎ}yY$$
5		cbviuneq12df.xa	$$⊢\underset{\_}{Ⅎ}xA$$
6		cbviuneq12df.ya	$$⊢\underset{\_}{Ⅎ}yA$$
7		cbviuneq12df.b	$$⊢\underset{\_}{Ⅎ}yB$$
8		cbviuneq12df.xc	$$⊢\underset{\_}{Ⅎ}xC$$
9		cbviuneq12df.yc	$$⊢\underset{\_}{Ⅎ}yC$$
10		cbviuneq12df.d	$$⊢\underset{\_}{Ⅎ}xD$$
11		cbviuneq12df.f	$$⊢\underset{\_}{Ⅎ}xF$$
12		cbviuneq12df.g	$$⊢\underset{\_}{Ⅎ}yG$$
13		cbviuneq12df.xel	$$⊢\left(\phi \wedge y\in C\right)\to X\in A$$
14		cbviuneq12df.yel	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
15		cbviuneq12df.xsub	$$⊢\left(\phi \wedge y\in C\wedge x=X\right)\to B=F$$
16		cbviuneq12df.ysub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
17		cbviuneq12df.eq1	$$⊢\left(\phi \wedge x\in A\right)\to B=G$$
18		cbviuneq12df.eq2	$$⊢\left(\phi \wedge y\in C\right)\to D=F$$
19		eqimss	$$⊢B=G\to B\subseteq G$$
20	17 19	syl	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq G$$
21	1 2 4 6 7 8 9 10 12 14 16 20	ss2iundf	$$⊢\phi \to \bigcup _{x\in A}B\subseteq \bigcup _{y\in C}D$$
22		eqimss	$$⊢D=F\to D\subseteq F$$
23	18 22	syl	$$⊢\left(\phi \wedge y\in C\right)\to D\subseteq F$$
24	2 1 3 8 10 6 5 7 11 13 15 23	ss2iundf	$$⊢\phi \to \bigcup _{y\in C}D\subseteq \bigcup _{x\in A}B$$
25	21 24	eqssd	$$⊢\phi \to \bigcup _{x\in A}B=\bigcup _{y\in C}D$$