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	⊢ ∅ ∈ dom vol
2		mblvol	⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
3	1 2	ax-mp	⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
4		ovol0	⊢ ( vol* ‘ ∅ ) = 0
5	3 4	eqtri	⊢ ( vol ‘ ∅ ) = 0