Theorem rabun2

Description: Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015)

	Ref	Expression
Assertion	rabun2	|- { x e. ( A u. B ) | ph } = ( { x e. A | ph } u. { x e. B | ph } )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. ( A u. B ) | ph } = { x | ( x e. ( A u. B ) /\ ph ) }
2		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
3		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
4	2 3	uneq12i	|- ( { x e. A | ph } u. { x e. B | ph } ) = ( { x | ( x e. A /\ ph ) } u. { x | ( x e. B /\ ph ) } )
5		elun	|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
6	5	anbi1i	|- ( ( x e. ( A u. B ) /\ ph ) <-> ( ( x e. A \/ x e. B ) /\ ph ) )
7		andir	|- ( ( ( x e. A \/ x e. B ) /\ ph ) <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) )
8	6 7	bitri	|- ( ( x e. ( A u. B ) /\ ph ) <-> ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) )
9	8	abbii	|- { x | ( x e. ( A u. B ) /\ ph ) } = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) }
10		unab	|- ( { x | ( x e. A /\ ph ) } u. { x | ( x e. B /\ ph ) } ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ ph ) ) }
11	9 10	eqtr4i	|- { x | ( x e. ( A u. B ) /\ ph ) } = ( { x | ( x e. A /\ ph ) } u. { x | ( x e. B /\ ph ) } )
12	4 11	eqtr4i	|- ( { x e. A | ph } u. { x e. B | ph } ) = { x | ( x e. ( A u. B ) /\ ph ) }
13	1 12	eqtr4i	|- { x e. ( A u. B ) | ph } = ( { x e. A | ph } u. { x e. B | ph } )