Theorem rabiun

Description: Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017)

	Ref	Expression
Assertion	rabiun	|- { x e. U_ y e. A B | ph } = U_ y e. A { x e. B | ph }

Proof

Step	Hyp	Ref	Expression
1		eliun	|- ( x e. U_ y e. A B <-> E. y e. A x e. B )
2	1	anbi1i	|- ( ( x e. U_ y e. A B /\ ph ) <-> ( E. y e. A x e. B /\ ph ) )
3		r19.41v	|- ( E. y e. A ( x e. B /\ ph ) <-> ( E. y e. A x e. B /\ ph ) )
4	2 3	bitr4i	|- ( ( x e. U_ y e. A B /\ ph ) <-> E. y e. A ( x e. B /\ ph ) )
5	4	abbii	|- { x | ( x e. U_ y e. A B /\ ph ) } = { x | E. y e. A ( x e. B /\ ph ) }
6		df-rab	|- { x e. U_ y e. A B | ph } = { x | ( x e. U_ y e. A B /\ ph ) }
7		iunab	|- U_ y e. A { x | ( x e. B /\ ph ) } = { x | E. y e. A ( x e. B /\ ph ) }
8	5 6 7	3eqtr4i	|- { x e. U_ y e. A B | ph } = U_ y e. A { x | ( x e. B /\ ph ) }
9		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
10	9	a1i	|- ( y e. A -> { x e. B | ph } = { x | ( x e. B /\ ph ) } )
11	10	iuneq2i	|- U_ y e. A { x e. B | ph } = U_ y e. A { x | ( x e. B /\ ph ) }
12	8 11	eqtr4i	|- { x e. U_ y e. A B | ph } = U_ y e. A { x e. B | ph }