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	$⊢ F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ$

Step	Hyp	Ref	Expression
1		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
2		dvfg	$⊢ ℂ \in \{ℝ, ℂ\} \to F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ$
3	1 2	ax-mp	$⊢ F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ$