Theorem iunrdx

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

	Ref	Expression
Hypotheses	iunrdx.1	|- ( ph -> F : A -onto-> C )
	iunrdx.2	|- ( ( ph /\ y = ( F ` x ) ) -> D = B )
Assertion	iunrdx	|- ( ph -> U_ x e. A B = U_ y e. C D )

Proof

Step	Hyp	Ref	Expression
1		iunrdx.1	|- ( ph -> F : A -onto-> C )
2		iunrdx.2	|- ( ( ph /\ y = ( F ` x ) ) -> D = B )
3		fof	|- ( F : A -onto-> C -> F : A --> C )
4	1 3	syl	|- ( ph -> F : A --> C )
5	4	ffvelrnda	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. C )
6		foelrn	|- ( ( F : A -onto-> C /\ y e. C ) -> E. x e. A y = ( F ` x ) )
7	1 6	sylan	|- ( ( ph /\ y e. C ) -> E. x e. A y = ( F ` x ) )
8	2	eleq2d	|- ( ( ph /\ y = ( F ` x ) ) -> ( z e. D <-> z e. B ) )
9	5 7 8	rexxfrd	|- ( ph -> ( E. y e. C z e. D <-> E. x e. A z e. B ) )
10	9	bicomd	|- ( ph -> ( E. x e. A z e. B <-> E. y e. C z e. D ) )
11	10	abbidv	|- ( ph -> { z | E. x e. A z e. B } = { z | E. y e. C z e. D } )
12		df-iun	|- U_ x e. A B = { z | E. x e. A z e. B }
13		df-iun	|- U_ y e. C D = { z | E. y e. C z e. D }
14	11 12 13	3eqtr4g	|- ( ph -> U_ x e. A B = U_ y e. C D )