Theorem rembl

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

	Ref	Expression
Assertion	rembl	$$⊢ℝ\in \mathrm{dom}vol$$

Proof

Step	Hyp	Ref	Expression
1		dif0	$$⊢ℝ\setminus \varnothing =ℝ$$
2		0mbl	$$⊢\varnothing \in \mathrm{dom}vol$$
3		cmmbl	$$⊢\varnothing \in \mathrm{dom}vol\to ℝ\setminus \varnothing \in \mathrm{dom}vol$$
4	2 3	ax-mp	$$⊢ℝ\setminus \varnothing \in \mathrm{dom}vol$$
5	1 4	eqeltrri	$$⊢ℝ\in \mathrm{dom}vol$$