This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralun

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

Ref Expression
Assertion ralun ⊢ ∀ x ∈ A φ ∧ ∀ x ∈ B φ → ∀ x ∈ A ∪ B φ

Proof

Step Hyp Ref Expression
1 ralunb ⊢ ∀ x ∈ A ∪ B φ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ B φ
2 1 biimpri ⊢ ∀ x ∈ A φ ∧ ∀ x ∈ B φ → ∀ x ∈ A ∪ B φ