Theorem iunrdx

Description: Re-index an indexed union. (Contributed by Thierry Arnoux, 6-Apr-2017)

	Ref	Expression
Hypotheses	iunrdx.1	$$⊢\phi \to F:A\underset{onto}{⟶}C$$
	iunrdx.2	$$⊢\left(\phi \wedge y=F\left(x\right)\right)\to D=B$$
Assertion	iunrdx	$$⊢\phi \to \bigcup _{x\in A}B=\bigcup _{y\in C}D$$

Proof

Step	Hyp	Ref	Expression
1		iunrdx.1	$$⊢\phi \to F:A\underset{onto}{⟶}C$$
2		iunrdx.2	$$⊢\left(\phi \wedge y=F\left(x\right)\right)\to D=B$$
3		fof	$$⊢F:A\underset{onto}{⟶}C\to F:A⟶C$$
4	1 3	syl	$$⊢\phi \to F:A⟶C$$
5	4	ffvelrnda	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in C$$
6		foelrn	$$⊢\left(F:A\underset{onto}{⟶}C\wedge y\in C\right)\to \exists x\in Ay=F\left(x\right)$$
7	1 6	sylan	$$⊢\left(\phi \wedge y\in C\right)\to \exists x\in Ay=F\left(x\right)$$
8	2	eleq2d	$$⊢\left(\phi \wedge y=F\left(x\right)\right)\to \left(z\in D\leftrightarrow z\in B\right)$$
9	5 7 8	rexxfrd	$$⊢\phi \to \left(\exists y\in Cz\in D\leftrightarrow \exists x\in Az\in B\right)$$
10	9	bicomd	$$⊢\phi \to \left(\exists x\in Az\in B\leftrightarrow \exists y\in Cz\in D\right)$$
11	10	abbidv	$$⊢\phi \to \left\{z|\exists x\in Az\in B\right\}=\left\{z|\exists y\in Cz\in D\right\}$$
12		df-iun	$$⊢\bigcup _{x\in A}B=\left\{z|\exists x\in Az\in B\right\}$$
13		df-iun	$$⊢\bigcup _{y\in C}D=\left\{z|\exists y\in Cz\in D\right\}$$
14	11 12 13	3eqtr4g	$$⊢\phi \to \bigcup _{x\in A}B=\bigcup _{y\in C}D$$