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