Step |
Hyp |
Ref |
Expression |
1 |
|
funimass4 |
|- ( ( Fun F /\ ( A X. B ) C_ dom F ) -> ( ( F " ( A X. B ) ) C_ C <-> A. z e. ( A X. B ) ( F ` z ) e. C ) ) |
2 |
|
fveq2 |
|- ( z = <. x , y >. -> ( F ` z ) = ( F ` <. x , y >. ) ) |
3 |
|
df-ov |
|- ( x F y ) = ( F ` <. x , y >. ) |
4 |
2 3
|
eqtr4di |
|- ( z = <. x , y >. -> ( F ` z ) = ( x F y ) ) |
5 |
4
|
eleq1d |
|- ( z = <. x , y >. -> ( ( F ` z ) e. C <-> ( x F y ) e. C ) ) |
6 |
5
|
ralxp |
|- ( A. z e. ( A X. B ) ( F ` z ) e. C <-> A. x e. A A. y e. B ( x F y ) e. C ) |
7 |
1 6
|
bitrdi |
|- ( ( Fun F /\ ( A X. B ) C_ dom F ) -> ( ( F " ( A X. B ) ) C_ C <-> A. x e. A A. y e. B ( x F y ) e. C ) ) |