Metamath Proof Explorer

Theorem dvf

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

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

Proof

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