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	$$⊢F_{ℝ}^{\prime }:\mathrm{dom}{F}_{ℝ}^{\prime }⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		reelprrecn	$$⊢ℝ\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 }⟶ℂ$$