This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0mbl

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

		Ref	Expression
	Assertion	0mbl	$⊢ \emptyset \in dom vol$

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