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ψ