Metamath Proof Explorer

Theorem 0mbl

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

Ref Expression
Assertion 0mbl 
|- (/) e. dom vol

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ RR
2 ovol0 
 |-  ( vol* ` (/) ) = 0
3 nulmbl 
 |-  ( ( (/) C_ RR /\ ( vol* ` (/) ) = 0 ) -> (/) e. dom vol )
4 1 2 3 mp2an 
 |-  (/) e. dom vol