Theorem 0mbl

Description: The empty set is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

	Ref	Expression
Assertion	0mbl	$$⊢\varnothing \in \mathrm{dom}vol$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq ℝ$$
2		ovol0	$$⊢{vol}^{*}\left(\varnothing \right)=0$$
3		nulmbl	$$⊢\left(\varnothing \subseteq ℝ\wedge {vol}^{*}\left(\varnothing \right)=0\right)\to \varnothing \in \mathrm{dom}vol$$
4	1 2 3	mp2an	$$⊢\varnothing \in \mathrm{dom}vol$$