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 )