This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absfun

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

		Ref	Expression
	Assertion	absfun	$⊢ Fun abs$

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