Metamath Proof Explorer

Theorem 2ralor

Description: Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Assertion 2ralor ⊢ ∀ x ∈ A ∀ y ∈ B φ ∨ ψ ↔ ∀ x ∈ A φ ∨ ∀ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 rexnal ⊢ ∃ x ∈ A ¬ φ ↔ ¬ ∀ x ∈ A φ
2 rexnal ⊢ ∃ y ∈ B ¬ ψ ↔ ¬ ∀ y ∈ B ψ
3 1 2 anbi12i ⊢ ∃ x ∈ A ¬ φ ∧ ∃ y ∈ B ¬ ψ ↔ ¬ ∀ x ∈ A φ ∧ ¬ ∀ y ∈ B ψ
4 ioran ⊢ ¬ φ ∨ ψ ↔ ¬ φ ∧ ¬ ψ
5 4 rexbii ⊢ ∃ y ∈ B ¬ φ ∨ ψ ↔ ∃ y ∈ B ¬ φ ∧ ¬ ψ
6 rexnal ⊢ ∃ y ∈ B ¬ φ ∨ ψ ↔ ¬ ∀ y ∈ B φ ∨ ψ
7 5 6 bitr3i ⊢ ∃ y ∈ B ¬ φ ∧ ¬ ψ ↔ ¬ ∀ y ∈ B φ ∨ ψ
8 7 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B ¬ φ ∧ ¬ ψ ↔ ∃ x ∈ A ¬ ∀ y ∈ B φ ∨ ψ
9 reeanv ⊢ ∃ x ∈ A ∃ y ∈ B ¬ φ ∧ ¬ ψ ↔ ∃ x ∈ A ¬ φ ∧ ∃ y ∈ B ¬ ψ
10 rexnal ⊢ ∃ x ∈ A ¬ ∀ y ∈ B φ ∨ ψ ↔ ¬ ∀ x ∈ A ∀ y ∈ B φ ∨ ψ
11 8 9 10 3bitr3ri ⊢ ¬ ∀ x ∈ A ∀ y ∈ B φ ∨ ψ ↔ ∃ x ∈ A ¬ φ ∧ ∃ y ∈ B ¬ ψ
12 ioran ⊢ ¬ ∀ x ∈ A φ ∨ ∀ y ∈ B ψ ↔ ¬ ∀ x ∈ A φ ∧ ¬ ∀ y ∈ B ψ
13 3 11 12 3bitr4i ⊢ ¬ ∀ x ∈ A ∀ y ∈ B φ ∨ ψ ↔ ¬ ∀ x ∈ A φ ∨ ∀ y ∈ B ψ
14 13 con4bii ⊢ ∀ x ∈ A ∀ y ∈ B φ ∨ ψ ↔ ∀ x ∈ A φ ∨ ∀ y ∈ B ψ