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 φ x B A C = D
mbfeqa.4 φ x B C
mbfeqa.5 φ x B D
Assertion mbfeqa φ x B C MblFn x B D MblFn

Proof

Step Hyp Ref Expression
1 mbfeqa.1 φ A
2 mbfeqa.2 φ vol * A = 0
3 mbfeqa.3 φ x B A C = D
4 mbfeqa.4 φ x B C
5 mbfeqa.5 φ x B D
6 3 fveq2d φ x B A C = D
7 4 recld φ x B C
8 5 recld φ x B D
9 1 2 6 7 8 mbfeqalem2 φ x B C MblFn x B D MblFn
10 3 fveq2d φ x B A C = D
11 4 imcld φ x B C
12 5 imcld φ x B D
13 1 2 10 11 12 mbfeqalem2 φ x B C MblFn x B D MblFn
14 9 13 anbi12d φ x B C MblFn x B C MblFn x B D MblFn x B D MblFn
15 4 ismbfcn2 φ x B C MblFn x B C MblFn x B C MblFn
16 5 ismbfcn2 φ x B D MblFn x B D MblFn x B D MblFn
17 14 15 16 3bitr4d φ x B C MblFn x B D MblFn