Metamath Proof Explorer

Theorem hlimeui

Description: The limit of a Hilbert space sequence is unique. (Contributed by NM, 19-Aug-1999) (Proof shortened by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlimeui ⊢ ∃ x F ⇝v x ↔ ∃! x F ⇝v x

Proof

Step Hyp Ref Expression
1 hlimreui ⊢ ∃ x ∈ V F ⇝v x ↔ ∃! x ∈ V F ⇝v x
2 rexv ⊢ ∃ x ∈ V F ⇝v x ↔ ∃ x F ⇝v x
3 reuv ⊢ ∃! x ∈ V F ⇝v x ↔ ∃! x F ⇝v x
4 1 2 3 3bitr3i ⊢ ∃ x F ⇝v x ↔ ∃! x F ⇝v x