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

Metamath Proof Explorer

Theorem r19.32v

Description: Restricted quantifier version of 19.32v . (Contributed by NM, 25-Nov-2003)

Ref Expression
Assertion r19.32v ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∀ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 r19.21v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )
2 df-or ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 → 𝜓 ) )
3 2 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜑 → 𝜓 ) )
4 df-or ⊢ ( ( 𝜑 ∨ ∀ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ¬ 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 ) )
5 1 3 4 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∀ 𝑥 ∈ 𝐴 𝜓 ) )