Theorem absfun

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

	Ref	Expression
Assertion	absfun	⊢ Fun abs

Proof

Step	Hyp	Ref	Expression
1		absf	⊢ abs : ℂ ⟶ ℝ
2		ffun	⊢ ( abs : ℂ ⟶ ℝ → Fun abs )
3	1 2	ax-mp	⊢ Fun abs