Step |
Hyp |
Ref |
Expression |
1 |
|
simp3 |
|- ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> B e. RR ) |
2 |
|
rexr |
|- ( B e. RR -> B e. RR* ) |
3 |
|
iccid |
|- ( B e. RR* -> ( B [,] B ) = { B } ) |
4 |
1 2 3
|
3syl |
|- ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( B [,] B ) = { B } ) |
5 |
4
|
imaeq2d |
|- ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " ( B [,] B ) ) = ( `' F " { B } ) ) |
6 |
|
mbfimaicc |
|- ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ B e. RR ) ) -> ( `' F " ( B [,] B ) ) e. dom vol ) |
7 |
6
|
anabsan2 |
|- ( ( ( F e. MblFn /\ F : A --> RR ) /\ B e. RR ) -> ( `' F " ( B [,] B ) ) e. dom vol ) |
8 |
7
|
3impa |
|- ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " ( B [,] B ) ) e. dom vol ) |
9 |
5 8
|
eqeltrrd |
|- ( ( F e. MblFn /\ F : A --> RR /\ B e. RR ) -> ( `' F " { B } ) e. dom vol ) |