Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | reurex | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reu5 | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ) | |
2 | 1 | simplbi | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) |