This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in dom vol \to A \subseteq ℝ$

Step	Hyp	Ref	Expression
1		ismbl	$⊢ A \in dom vol \leftrightarrow (A \subseteq ℝ \land \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x) = {vol}^{} (x \cap A) + {vol}^{} (x ∖ A)))$
2	1	simplbi	$⊢ A \in dom vol \to A \subseteq ℝ$