Theorem absex

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

	Ref	Expression
Assertion	absex	$$⊢\mathrm{abs}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3		reex	$$⊢ℝ\in \mathrm{V}$$
4		fex2	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℂ\in \mathrm{V}\wedge ℝ\in \mathrm{V}\right)\to \mathrm{abs}\in \mathrm{V}$$
5	1 2 3 4	mp3an	$$⊢\mathrm{abs}\in \mathrm{V}$$