Step |
Hyp |
Ref |
Expression |
1 |
|
elovimad.1 |
|- ( ph -> A e. C ) |
2 |
|
elovimad.2 |
|- ( ph -> B e. D ) |
3 |
|
elovimad.3 |
|- ( ph -> Fun F ) |
4 |
|
elovimad.4 |
|- ( ph -> ( C X. D ) C_ dom F ) |
5 |
|
df-ov |
|- ( A F B ) = ( F ` <. A , B >. ) |
6 |
1 2
|
opelxpd |
|- ( ph -> <. A , B >. e. ( C X. D ) ) |
7 |
4 6
|
sseldd |
|- ( ph -> <. A , B >. e. dom F ) |
8 |
|
funfvima |
|- ( ( Fun F /\ <. A , B >. e. dom F ) -> ( <. A , B >. e. ( C X. D ) -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) ) ) |
9 |
3 7 8
|
syl2anc |
|- ( ph -> ( <. A , B >. e. ( C X. D ) -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) ) ) |
10 |
6 9
|
mpd |
|- ( ph -> ( F ` <. A , B >. ) e. ( F " ( C X. D ) ) ) |
11 |
5 10
|
eqeltrid |
|- ( ph -> ( A F B ) e. ( F " ( C X. D ) ) ) |