Theorem iuneq12daf

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iuneq12daf.1	$$⊢Ⅎx\phi$$
2		iuneq12daf.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		iuneq12daf.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		iuneq12daf.4	$$⊢\phi \to A=B$$
5		iuneq12daf.5	$$⊢\left(\phi \wedge x\in A\right)\to C=D$$
6	5	eleq2d	$$⊢\left(\phi \wedge x\in A\right)\to \left(y\in C\leftrightarrow y\in D\right)$$
7	1 6	rexbida	$$⊢\phi \to \left(\exists x\in Ay\in C\leftrightarrow \exists x\in Ay\in D\right)$$
8	2 3	rexeqf	$$⊢A=B\to \left(\exists x\in Ay\in D\leftrightarrow \exists x\in By\in D\right)$$
9	4 8	syl	$$⊢\phi \to \left(\exists x\in Ay\in D\leftrightarrow \exists x\in By\in D\right)$$
10	7 9	bitrd	$$⊢\phi \to \left(\exists x\in Ay\in C\leftrightarrow \exists x\in By\in D\right)$$
11	10	alrimiv	$$⊢\phi \to \forall y\left(\exists x\in Ay\in C\leftrightarrow \exists x\in By\in D\right)$$
12		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\}$$
13		df-iun	$$⊢\bigcup _{x\in A}C=\left\{y|\exists x\in Ay\in C\right\}$$
14		df-iun	$$⊢\bigcup _{x\in B}D=\left\{y|\exists x\in By\in D\right\}$$
15	12 13 14	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$$
16	11 15	syl	$$⊢\phi \to \bigcup _{x\in A}C=\bigcup _{x\in B}D$$