Metamath Proof Explorer

Theorem mblss

Description: A measurable set is a subset of the reals. (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion mblss 
|- ( A e. dom vol -> A C_ RR )

Proof

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 )