Theorem sgndm

Description: The domain of the signum function. (Contributed by AV, 16-Jun-2026)

	Ref	Expression
Assertion	sgndm	⊢ dom sgn = ℝ*

Proof

Step	Hyp	Ref	Expression
1		c0ex	⊢ 0 ∈ V
2		negex	⊢ - 1 ∈ V
3		1ex	⊢ 1 ∈ V
4	2 3	ifex	⊢ if ( 𝑥 < 0 , - 1 , 1 ) ∈ V
5	1 4	ifex	⊢ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) ∈ V
6		df-sgn	⊢ sgn = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) )
7	5 6	dmmpti	⊢ dom sgn = ℝ*