Metamath Proof Explorer

Theorem absf

Description: Mapping domain and codomain of the absolute value function. (Contributed by NM, 30-Aug-2007) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion absf abs :


Step Hyp Ref Expression
1 df-abs abs = x x x
2 absval x x = x x
3 abscl x x
4 2 3 eqeltrrd x x x
5 1 4 fmpti abs :