Theorem ralun

Description: Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	ralun	|- ( ( A. x e. A ph /\ A. x e. B ph ) -> A. x e. ( A u. B ) ph )

Proof

Step	Hyp	Ref	Expression
1		ralunb	|- ( A. x e. ( A u. B ) ph <-> ( A. x e. A ph /\ A. x e. B ph ) )
2	1	biimpri	|- ( ( A. x e. A ph /\ A. x e. B ph ) -> A. x e. ( A u. B ) ph )