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 | |
|
mbfeqa.2 | |
||
mbfeqa.3 | |
||
mbfeqa.4 | |
||
mbfeqa.5 | |
||
Assertion | mbfeqa | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mbfeqa.1 | |
|
2 | mbfeqa.2 | |
|
3 | mbfeqa.3 | |
|
4 | mbfeqa.4 | |
|
5 | mbfeqa.5 | |
|
6 | 3 | fveq2d | |
7 | 4 | recld | |
8 | 5 | recld | |
9 | 1 2 6 7 8 | mbfeqalem2 | |
10 | 3 | fveq2d | |
11 | 4 | imcld | |
12 | 5 | imcld | |
13 | 1 2 10 11 12 | mbfeqalem2 | |
14 | 9 13 | anbi12d | |
15 | 4 | ismbfcn2 | |
16 | 5 | ismbfcn2 | |
17 | 14 15 16 | 3bitr4d | |