Theorem iuneq12df

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016)

	Ref	Expression
Hypotheses	iuneq12df.1	$$⊢Ⅎx\phi$$
	iuneq12df.2	$$⊢\underset{\_}{Ⅎ}xA$$
	iuneq12df.3	$$⊢\underset{\_}{Ⅎ}xB$$
	iuneq12df.4	$$⊢\phi \to A=B$$
	iuneq12df.5	$$⊢\phi \to C=D$$
Assertion	iuneq12df	$$⊢\phi \to \bigcup _{x\in A}C=\bigcup _{x\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		iuneq12df.1	$$⊢Ⅎx\phi$$
2		iuneq12df.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		iuneq12df.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		iuneq12df.4	$$⊢\phi \to A=B$$
5		iuneq12df.5	$$⊢\phi \to C=D$$
6	5	eleq2d	$$⊢\phi \to \left(y\in C\leftrightarrow y\in D\right)$$
7	1 2 3 4 6	rexeqbid	$$⊢\phi \to \left(\exists x\in Ay\in C\leftrightarrow \exists x\in By\in D\right)$$
8	7	alrimiv	$$⊢\phi \to \forall y\left(\exists x\in Ay\in C\leftrightarrow \exists x\in By\in D\right)$$
9		abbi1	$$⊢\forall y\left(\exists x\in Ay\in C\leftrightarrow \exists x\in By\in D\right)\to \left\{y|\exists x\in Ay\in C\right\}=\left\{y|\exists x\in By\in D\right\}$$
10		df-iun	$$⊢\bigcup _{x\in A}C=\left\{y|\exists x\in Ay\in C\right\}$$
11		df-iun	$$⊢\bigcup _{x\in B}D=\left\{y|\exists x\in By\in D\right\}$$
12	9 10 11	3eqtr4g	$$⊢\forall y\left(\exists x\in Ay\in C\leftrightarrow \exists x\in By\in D\right)\to \bigcup _{x\in A}C=\bigcup _{x\in B}D$$
13	8 12	syl	$$⊢\phi \to \bigcup _{x\in A}C=\bigcup _{x\in B}D$$