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

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 ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 elunant ⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 → 𝜑 ) ) )
2 1 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → 𝜑 ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 → 𝜑 ) ) )
3 19.26 ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 → 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) ) )
4 2 3 bitri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) ) )
5 df-ral ⊢ ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → 𝜑 ) )
6 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
7 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) )
8 6 7 anbi12i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) ↔ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝜑 ) ) )
9 4 5 8 3bitr4i ⊢ ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )