Theorem vol0

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

	Ref	Expression
Assertion	vol0	$$⊢vol\left(\varnothing \right)=0$$

Proof

Step	Hyp	Ref	Expression
1		0mbl	$$⊢\varnothing \in \mathrm{dom}vol$$
2		mblvol	$$⊢\varnothing \in \mathrm{dom}vol\to vol\left(\varnothing \right)={vol}^{*}\left(\varnothing \right)$$
3	1 2	ax-mp	$$⊢vol\left(\varnothing \right)={vol}^{*}\left(\varnothing \right)$$
4		ovol0	$$⊢{vol}^{*}\left(\varnothing \right)=0$$
5	3 4	eqtri	$$⊢vol\left(\varnothing \right)=0$$