Metamath Proof Explorer

Theorem 2ralor

Description: Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Wolf Lammen, 20-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 r19.32v ⊢ ∀ y ∈ B φ ∨ ψ ↔ φ ∨ ∀ y ∈ B ψ
2 orcom ⊢ φ ∨ ∀ y ∈ B ψ ↔ ∀ y ∈ B ψ ∨ φ
3 1 2 bitri ⊢ ∀ y ∈ B φ ∨ ψ ↔ ∀ y ∈ B ψ ∨ φ
4 3 ralbii ⊢ ∀ x ∈ A ∀ y ∈ B φ ∨ ψ ↔ ∀ x ∈ A ∀ y ∈ B ψ ∨ φ
5 r19.32v ⊢ ∀ x ∈ A ∀ y ∈ B ψ ∨ φ ↔ ∀ y ∈ B ψ ∨ ∀ x ∈ A φ
6 orcom ⊢ ∀ y ∈ B ψ ∨ ∀ x ∈ A φ ↔ ∀ x ∈ A φ ∨ ∀ y ∈ B ψ
7 4 5 6 3bitri ⊢ ∀ x ∈ A ∀ y ∈ B φ ∨ ψ ↔ ∀ x ∈ A φ ∨ ∀ y ∈ B ψ