Metamath Proof Explorer

Theorem absex

Description: The absolute value function is a set. (Contributed by SN, 5-Jun-2025)

Ref Expression
Assertion absex 
|- abs e. _V

Proof

Step Hyp Ref Expression
1 absf 
 |-  abs : CC --> RR
2 cnex 
 |-  CC e. _V
3 reex 
 |-  RR e. _V
4 fex2 
 |-  ( ( abs : CC --> RR /\ CC e. _V /\ RR e. _V ) -> abs e. _V )
5 1 2 3 4 mp3an 
 |-  abs e. _V