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 ⊢∀xx∈A∪B→φ↔∀xx∈A→φ∧x∈B→φ
3 19.26 ⊢∀xx∈A→φ∧x∈B→φ↔∀xx∈A→φ∧∀xx∈B→φ
4 2 3 bitri ⊢∀xx∈A∪B→φ↔∀xx∈A→φ∧∀xx∈B→φ
5 df-ral ⊢∀x∈A∪Bφ↔∀xx∈A∪B→φ
6 df-ral ⊢∀x∈Aφ↔∀xx∈A→φ
7 df-ral ⊢∀x∈Bφ↔∀xx∈B→φ
8 6 7 anbi12i ⊢∀x∈Aφ∧∀x∈Bφ↔∀xx∈A→φ∧∀xx∈B→φ
9 4 5 8 3bitr4i ⊢∀x∈A∪Bφ↔∀x∈Aφ∧∀x∈Bφ