Step |
Hyp |
Ref |
Expression |
1 |
|
mbfeqa.1 |
|- ( ph -> A C_ RR ) |
2 |
|
mbfeqa.2 |
|- ( ph -> ( vol* ` A ) = 0 ) |
3 |
|
mbfeqa.3 |
|- ( ( ph /\ x e. ( B \ A ) ) -> C = D ) |
4 |
|
mbfeqa.4 |
|- ( ( ph /\ x e. B ) -> C e. CC ) |
5 |
|
mbfeqa.5 |
|- ( ( ph /\ x e. B ) -> D e. CC ) |
6 |
3
|
fveq2d |
|- ( ( ph /\ x e. ( B \ A ) ) -> ( Re ` C ) = ( Re ` D ) ) |
7 |
4
|
recld |
|- ( ( ph /\ x e. B ) -> ( Re ` C ) e. RR ) |
8 |
5
|
recld |
|- ( ( ph /\ x e. B ) -> ( Re ` D ) e. RR ) |
9 |
1 2 6 7 8
|
mbfeqalem2 |
|- ( ph -> ( ( x e. B |-> ( Re ` C ) ) e. MblFn <-> ( x e. B |-> ( Re ` D ) ) e. MblFn ) ) |
10 |
3
|
fveq2d |
|- ( ( ph /\ x e. ( B \ A ) ) -> ( Im ` C ) = ( Im ` D ) ) |
11 |
4
|
imcld |
|- ( ( ph /\ x e. B ) -> ( Im ` C ) e. RR ) |
12 |
5
|
imcld |
|- ( ( ph /\ x e. B ) -> ( Im ` D ) e. RR ) |
13 |
1 2 10 11 12
|
mbfeqalem2 |
|- ( ph -> ( ( x e. B |-> ( Im ` C ) ) e. MblFn <-> ( x e. B |-> ( Im ` D ) ) e. MblFn ) ) |
14 |
9 13
|
anbi12d |
|- ( ph -> ( ( ( x e. B |-> ( Re ` C ) ) e. MblFn /\ ( x e. B |-> ( Im ` C ) ) e. MblFn ) <-> ( ( x e. B |-> ( Re ` D ) ) e. MblFn /\ ( x e. B |-> ( Im ` D ) ) e. MblFn ) ) ) |
15 |
4
|
ismbfcn2 |
|- ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( ( x e. B |-> ( Re ` C ) ) e. MblFn /\ ( x e. B |-> ( Im ` C ) ) e. MblFn ) ) ) |
16 |
5
|
ismbfcn2 |
|- ( ph -> ( ( x e. B |-> D ) e. MblFn <-> ( ( x e. B |-> ( Re ` D ) ) e. MblFn /\ ( x e. B |-> ( Im ` D ) ) e. MblFn ) ) ) |
17 |
14 15 16
|
3bitr4d |
|- ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) ) |