Description: A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17Mar2014)
Ref  Expression  

Assertion  mblss   ( A e. dom vol > A C_ RR ) 
Step  Hyp  Ref  Expression 

1  ismbl   ( A e. dom vol <> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR > ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) ) 

2  1  simplbi   ( A e. dom vol > A C_ RR ) 