Theorem climreu

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005)

	Ref	Expression
Assertion	climreu	$$⊢F⇝A\to \exists !x\in ℂF⇝x$$

Proof

Step	Hyp	Ref	Expression
1		climeu	$$⊢F⇝A\to \exists !xF⇝x$$
2		climcl	$$⊢F⇝x\to x\in ℂ$$
3	2	pm4.71ri	$$⊢F⇝x\leftrightarrow \left(x\in ℂ\wedge F⇝x\right)$$
4	3	eubii	$$⊢\exists !xF⇝x\leftrightarrow \exists !x\left(x\in ℂ\wedge F⇝x\right)$$
5		df-reu	$$⊢\exists !x\in ℂF⇝x\leftrightarrow \exists !x\left(x\in ℂ\wedge F⇝x\right)$$
6	4 5	bitr4i	$$⊢\exists !xF⇝x\leftrightarrow \exists !x\in ℂF⇝x$$
7	1 6	sylib	$$⊢F⇝A\to \exists !x\in ℂF⇝x$$