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 𝐹 ) ⟶ ℂ