Metamath Proof Explorer

Theorem ralunb

Description: Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion ralunb ⊢ ∀ x ∈ A ∪ B φ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ B φ

Proof

Step Hyp Ref Expression
1 elunant ⊢ x ∈ A ∪ B → φ ↔ x ∈ A → φ ∧ x ∈ B → φ
2 1 albii ⊢ ∀ x x ∈ A ∪ B → φ ↔ ∀ x x ∈ A → φ ∧ x ∈ B → φ
3 19.26 ⊢ ∀ x x ∈ A → φ ∧ x ∈ B → φ ↔ ∀ x x ∈ A → φ ∧ ∀ x x ∈ B → φ
4 2 3 bitri ⊢ ∀ x x ∈ A ∪ B → φ ↔ ∀ x x ∈ A → φ ∧ ∀ x x ∈ B → φ
5 df-ral ⊢ ∀ x ∈ A ∪ B φ ↔ ∀ x x ∈ A ∪ B → φ
6 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
7 df-ral ⊢ ∀ x ∈ B φ ↔ ∀ x x ∈ B → φ
8 6 7 anbi12i ⊢ ∀ x ∈ A φ ∧ ∀ x ∈ B φ ↔ ∀ x x ∈ A → φ ∧ ∀ x x ∈ B → φ
9 4 5 8 3bitr4i ⊢ ∀ x ∈ A ∪ B φ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ B φ