Theorem ralun

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

	Ref	Expression
Assertion	ralun	$$⊢\left(\forall x\in A\phi \wedge \forall x\in B\phi \right)\to \forall x\in \left(A\cup B\right)\phi$$

Proof

Step	Hyp	Ref	Expression
1		ralunb	$$⊢\forall x\in \left(A\cup B\right)\phi \leftrightarrow \left(\forall x\in A\phi \wedge \forall x\in B\phi \right)$$
2	1	biimpri	$$⊢\left(\forall x\in A\phi \wedge \forall x\in B\phi \right)\to \forall x\in \left(A\cup B\right)\phi$$