Metamath Proof Explorer


Theorem vol0

Description: The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion vol0
|- ( vol ` (/) ) = 0

Proof

Step Hyp Ref Expression
1 0mbl
 |-  (/) e. dom vol
2 mblvol
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
3 1 2 ax-mp
 |-  ( vol ` (/) ) = ( vol* ` (/) )
4 ovol0
 |-  ( vol* ` (/) ) = 0
5 3 4 eqtri
 |-  ( vol ` (/) ) = 0