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