Metamath Proof Explorer

Theorem hlimreui

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

Ref Expression
Assertion hlimreui 
|- ( E. x e. H F ~~>v x <-> E! x e. H F ~~>v x )

Proof

Step Hyp Ref Expression
1 hlimuni 
 |-  ( ( F ~~>v x /\ F ~~>v y ) -> x = y )
2 1 rgen2w 
 |-  A. x e. H A. y e. H ( ( F ~~>v x /\ F ~~>v y ) -> x = y )
3 2 biantru 
 |-  ( E. x e. H F ~~>v x <-> ( E. x e. H F ~~>v x /\ A. x e. H A. y e. H ( ( F ~~>v x /\ F ~~>v y ) -> x = y ) ) )
4 breq2 
 |-  ( x = y -> ( F ~~>v x <-> F ~~>v y ) )
5 4 reu4 
 |-  ( E! x e. H F ~~>v x <-> ( E. x e. H F ~~>v x /\ A. x e. H A. y e. H ( ( F ~~>v x /\ F ~~>v y ) -> x = y ) ) )
6 3 5 bitr4i 
 |-  ( E. x e. H F ~~>v x <-> E! x e. H F ~~>v x )