Description: Restricted version of Theorem 19.45 of Margaris p. 90. (Contributed by NM, 27-May-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | r19.45zv | ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.9rzv | ⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜑 ) ) | |
2 | 1 | orbi1d | ⊢ ( 𝐴 ≠ ∅ → ( ( 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) ) |
3 | r19.43 | ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) | |
4 | 2 3 | syl6rbbr | ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ) ) |