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 dom vol A


Step Hyp Ref Expression
1 ismbl A dom vol A x 𝒫 vol * x vol * x = vol * x A + vol * x A
2 1 simplbi A dom vol A