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 | |- ( E. x F ~~>v x <-> E! x F ~~>v x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlimreui | |- ( E. x e. _V F ~~>v x <-> E! x e. _V F ~~>v x ) |
|
| 2 | rexv | |- ( E. x e. _V F ~~>v x <-> E. x F ~~>v x ) |
|
| 3 | reuv | |- ( E! x e. _V F ~~>v x <-> E! x F ~~>v x ) |
|
| 4 | 1 2 3 | 3bitr3i | |- ( E. x F ~~>v x <-> E! x F ~~>v x ) |