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 ⊢ ∀ x ∈ A φ ∨ ψ ↔ φ ∨ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 r19.21v ⊢ ∀ x ∈ A ¬ φ → ψ ↔ ¬ φ → ∀ x ∈ A ψ
2 df-or ⊢ φ ∨ ψ ↔ ¬ φ → ψ
3 2 ralbii ⊢ ∀ x ∈ A φ ∨ ψ ↔ ∀ x ∈ A ¬ φ → ψ
4 df-or ⊢ φ ∨ ∀ x ∈ A ψ ↔ ¬ φ → ∀ x ∈ A ψ
5 1 3 4 3bitr4i ⊢ ∀ x ∈ A φ ∨ ψ ↔ φ ∨ ∀ x ∈ A ψ