Theorem rembl

Description: The set of all real numbers is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

	Ref	Expression
Assertion	rembl	⊢ ℝ ∈ dom vol

Proof

Step	Hyp	Ref	Expression
1		dif0	⊢ ( ℝ ∖ ∅ ) = ℝ
2		0mbl	⊢ ∅ ∈ dom vol
3		cmmbl	⊢ ( ∅ ∈ dom vol → ( ℝ ∖ ∅ ) ∈ dom vol )
4	2 3	ax-mp	⊢ ( ℝ ∖ ∅ ) ∈ dom vol
5	1 4	eqeltrri	⊢ ℝ ∈ dom vol