Theorem ralun

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

	Ref	Expression
Assertion	ralun	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ralunb	⊢ ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )
2	1	biimpri	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 )