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