Metamath Proof Explorer

Theorem mbf0

Description: The empty function is measurable. (Contributed by Brendan Leahy, 28-Mar-2018)

Ref Expression
Assertion mbf0 
|- (/) e. MblFn

Proof

Step Hyp Ref Expression
1 0xp 
 |-  ( (/) X. { 1 } ) = (/)
2 0mbl 
 |-  (/) e. dom vol
3 ax-1cn 
 |-  1 e. CC
4 mbfconst 
 |-  ( ( (/) e. dom vol /\ 1 e. CC ) -> ( (/) X. { 1 } ) e. MblFn )
5 2 3 4 mp2an 
 |-  ( (/) X. { 1 } ) e. MblFn
6 1 5 eqeltrri 
 |-  (/) e. MblFn