Theorem mblss

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

	Ref	Expression
Assertion	mblss	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ismbl	⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
2	1	simplbi	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )