Description: If a convergent function has its values in a Hausdorff space, then it has a unique limit. (Contributed by FL, 14-Nov-2010) (Revised by Stefan O'Rear, 6-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | hausflf.x | |
|
Assertion | hausflf2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hausflf.x | |
|
2 | n0 | |
|
3 | 2 | biimpi | |
4 | 1 | hausflf | |
5 | euen1b | |
|
6 | df-eu | |
|
7 | 5 6 | sylbbr | |
8 | 3 4 7 | syl2anr | |