Theorem volsn

Description: A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	volsn	⊢ ( 𝐴 ∈ ℝ → ( vol ‘ { 𝐴 } ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		snmbl	⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ∈ dom vol )
2		mblvol	⊢ ( { 𝐴 } ∈ dom vol → ( vol ‘ { 𝐴 } ) = ( vol* ‘ { 𝐴 } ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ → ( vol ‘ { 𝐴 } ) = ( vol* ‘ { 𝐴 } ) )
4		ovolsn	⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ { 𝐴 } ) = 0 )
5	3 4	eqtrd	⊢ ( 𝐴 ∈ ℝ → ( vol ‘ { 𝐴 } ) = 0 )