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

Metamath Proof Explorer

Theorem r19.44zv

Description: Restricted version of Theorem 19.44 of Margaris p. 90. (Contributed by NM, 27-May-1998)

Ref Expression
Assertion r19.44zv ⊢ A ≠ ∅ → ∃ x ∈ A φ ∨ ψ ↔ ∃ x ∈ A φ ∨ ψ

Proof

Step Hyp Ref Expression
1 r19.43 ⊢ ∃ x ∈ A φ ∨ ψ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ
2 r19.9rzv ⊢ A ≠ ∅ → ψ ↔ ∃ x ∈ A ψ
3 2 orbi2d ⊢ A ≠ ∅ → ∃ x ∈ A φ ∨ ψ ↔ ∃ x ∈ A φ ∨ ∃ x ∈ A ψ
4 1 3 bitr4id ⊢ A ≠ ∅ → ∃ x ∈ A φ ∨ ψ ↔ ∃ x ∈ A φ ∨ ψ