Metamath Proof Explorer

Theorem dvfcn

Description: The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Assertion dvfcn 
|- ( CC _D F ) : dom ( CC _D F ) --> CC

Proof

Step Hyp Ref Expression
1 cnelprrecn 
 |-  CC e. { RR , CC }
2 dvfg 
 |-  ( CC e. { RR , CC } -> ( CC _D F ) : dom ( CC _D F ) --> CC )
3 1 2 ax-mp 
 |-  ( CC _D F ) : dom ( CC _D F ) --> CC