This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvfcn

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

Ref Expression
Assertion dvfcn ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ

Proof

Step Hyp Ref Expression
1 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
2 dvfg ⊢ ( ℂ ∈ { ℝ , ℂ } → ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ )
3 1 2 ax-mp ⊢ ( ℂ D 𝐹 ) : dom ( ℂ D 𝐹 ) ⟶ ℂ