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	$$⊢{\exists }^{*}xF⇝x$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=y\to \left(F⇝x\leftrightarrow F⇝y\right)$$
2	1	cbvexvw	$$⊢\exists xF⇝x\leftrightarrow \exists yF⇝y$$
3		climeu	$$⊢F⇝y\to \exists !xF⇝x$$
4	3	exlimiv	$$⊢\exists yF⇝y\to \exists !xF⇝x$$
5	2 4	sylbi	$$⊢\exists xF⇝x\to \exists !xF⇝x$$
6		moeu	$$⊢{\exists }^{*}xF⇝x\leftrightarrow \left(\exists xF⇝x\to \exists !xF⇝x\right)$$
7	5 6	mpbir	$$⊢{\exists }^{*}xF⇝x$$