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

Metamath Proof Explorer

Theorem reurmo

Description: Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017)

Ref Expression
Assertion reurmo ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 reu5 ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) )
2 1 simprbi ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 )