Metamath Proof Explorer

Theorem ovolsn

Description: A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Assertion ovolsn 
|- ( A e. RR -> ( vol* ` { A } ) = 0 )

Proof

Step Hyp Ref Expression
1 snfi 
 |-  { A } e. Fin
2 snssi 
 |-  ( A e. RR -> { A } C_ RR )
3 ovolfi 
 |-  ( ( { A } e. Fin /\ { A } C_ RR ) -> ( vol* ` { A } ) = 0 )
4 1 2 3 sylancr 
 |-  ( A e. RR -> ( vol* ` { A } ) = 0 )