Metamath Proof Explorer

Theorem idcncf

Description: The identity function is a continuous function on CC . (Contributed by Jeff Madsen, 11-Jun-2010) (Moved into main as cncfmptid and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis idcncf.1 F = x x
Assertion idcncf F : cn


Step Hyp Ref Expression
1 idcncf.1 F = x x
2 ssid
3 cncfmptid x x : cn
4 2 2 3 mp2an x x : cn
5 1 4 eqeltri F : cn