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

Metamath Proof Explorer

Theorem r19.45zv

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

Ref Expression
Assertion r19.45zv ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 r19.43 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )
2 r19.9rzv ⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
3 2 orbi1d ⊢ ( 𝐴 ≠ ∅ → ( ( 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) )
4 1 3 bitr4id ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) )