Metamath Proof Explorer


Theorem climmo

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013)

Ref Expression
Assertion climmo
|- E* x F ~~> x

Proof

Step Hyp Ref Expression
1 breq2
 |-  ( x = y -> ( F ~~> x <-> F ~~> y ) )
2 1 cbvexvw
 |-  ( E. x F ~~> x <-> E. y F ~~> y )
3 climeu
 |-  ( F ~~> y -> E! x F ~~> x )
4 3 exlimiv
 |-  ( E. y F ~~> y -> E! x F ~~> x )
5 2 4 sylbi
 |-  ( E. x F ~~> x -> E! x F ~~> x )
6 moeu
 |-  ( E* x F ~~> x <-> ( E. x F ~~> x -> E! x F ~~> x ) )
7 5 6 mpbir
 |-  E* x F ~~> x