Metamath Proof Explorer


Theorem mbfeqa

Description: If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses mbfeqa.1 φA
mbfeqa.2 φvol*A=0
mbfeqa.3 φxBAC=D
mbfeqa.4 φxBC
mbfeqa.5 φxBD
Assertion mbfeqa φxBCMblFnxBDMblFn

Proof

Step Hyp Ref Expression
1 mbfeqa.1 φA
2 mbfeqa.2 φvol*A=0
3 mbfeqa.3 φxBAC=D
4 mbfeqa.4 φxBC
5 mbfeqa.5 φxBD
6 3 fveq2d φxBAC=D
7 4 recld φxBC
8 5 recld φxBD
9 1 2 6 7 8 mbfeqalem2 φxBCMblFnxBDMblFn
10 3 fveq2d φxBAC=D
11 4 imcld φxBC
12 5 imcld φxBD
13 1 2 10 11 12 mbfeqalem2 φxBCMblFnxBDMblFn
14 9 13 anbi12d φxBCMblFnxBCMblFnxBDMblFnxBDMblFn
15 4 ismbfcn2 φxBCMblFnxBCMblFnxBCMblFn
16 5 ismbfcn2 φxBDMblFnxBDMblFnxBDMblFn
17 14 15 16 3bitr4d φxBCMblFnxBDMblFn