Theorem absfun

Description: The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	absfun	$$⊢\mathrm{Fun}\mathrm{abs}$$

Proof

Step	Hyp	Ref	Expression
1		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
2		ffun	$$⊢\mathrm{abs}:ℂ⟶ℝ\to \mathrm{Fun}\mathrm{abs}$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}\mathrm{abs}$$