Metamath Proof Explorer


Theorem rembl

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

Ref Expression
Assertion rembl
|- RR e. dom vol

Proof

Step Hyp Ref Expression
1 dif0
 |-  ( RR \ (/) ) = RR
2 0mbl
 |-  (/) e. dom vol
3 cmmbl
 |-  ( (/) e. dom vol -> ( RR \ (/) ) e. dom vol )
4 2 3 ax-mp
 |-  ( RR \ (/) ) e. dom vol
5 1 4 eqeltrri
 |-  RR e. dom vol