Theorem 0mbl

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

	Ref	Expression
Assertion	0mbl	⊢ ∅ ∈ dom vol

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ℝ
2		ovol0	⊢ ( vol* ‘ ∅ ) = 0
3		nulmbl	⊢ ( ( ∅ ⊆ ℝ ∧ ( vol* ‘ ∅ ) = 0 ) → ∅ ∈ dom vol )
4	1 2 3	mp2an	⊢ ∅ ∈ dom vol