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 ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 r19.32v ( ∀ 𝑦𝐵 ( 𝜑𝜓 ) ↔ ( 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) )
2 orcom ( ( 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) ↔ ( ∀ 𝑦𝐵 𝜓𝜑 ) )
3 1 2 bitri ( ∀ 𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑦𝐵 𝜓𝜑 ) )
4 3 ralbii ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 𝜓𝜑 ) )
5 r19.32v ( ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 𝜓𝜑 ) ↔ ( ∀ 𝑦𝐵 𝜓 ∨ ∀ 𝑥𝐴 𝜑 ) )
6 orcom ( ( ∀ 𝑦𝐵 𝜓 ∨ ∀ 𝑥𝐴 𝜑 ) ↔ ( ∀ 𝑥𝐴 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) )
7 4 5 6 3bitri ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 ∨ ∀ 𝑦𝐵 𝜓 ) )