Metamath Proof Explorer

Theorem mbfdmssre

Description: The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion mbfdmssre F MblFn dom F


Step Hyp Ref Expression
1 ismbf1 F MblFn F 𝑝𝑚 x ran . F -1 x dom vol F -1 x dom vol
2 1 simplbi F MblFn F 𝑝𝑚
3 elpmi2 F 𝑝𝑚 dom F
4 2 3 syl F MblFn dom F