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

Metamath Proof Explorer

Theorem absex

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

Ref Expression
Assertion absex ⊢ abs ∈ V

Proof

Step Hyp Ref Expression
1 absf ⊢ abs : ℂ ⟶ ℝ
2 cnex ⊢ ℂ ∈ V
3 reex ⊢ ℝ ∈ V
4 fex2 ⊢ abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ∧ ℝ ∈ V → abs ∈ V
5 1 2 3 4 mp3an ⊢ abs ∈ V