Metamath Proof Explorer


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 )