Metamath Proof Explorer


Theorem volsn

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

Ref Expression
Assertion volsn AvolA=0

Proof

Step Hyp Ref Expression
1 snmbl AAdomvol
2 mblvol AdomvolvolA=vol*A
3 1 2 syl AvolA=vol*A
4 ovolsn Avol*A=0
5 3 4 eqtrd AvolA=0