Theorem iunrab

Description: The indexed union of a restricted class abstraction. (Contributed by NM, 3-Jan-2004) (Proof shortened by Mario Carneiro, 14-Nov-2016)

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

Proof

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