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	⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ

Proof

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