Theorem dvfcn

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

	Ref	Expression
Assertion	dvfcn	$$⊢F_{ℂ}^{\prime }:\mathrm{dom}{F}_{ℂ}^{\prime }⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
2		dvfg	$$⊢ℂ\in \left\{ℝ,ℂ\right\}\to F_{ℂ}^{\prime }:\mathrm{dom}{F}_{ℂ}^{\prime }⟶ℂ$$
3	1 2	ax-mp	$$⊢F_{ℂ}^{\prime }:\mathrm{dom}{F}_{ℂ}^{\prime }⟶ℂ$$