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