Metamath Proof Explorer

Theorem ovelimab

Description: Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013) (Revised by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion ovelimab 
|- ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( D e. ( F " ( B X. C ) ) <-> E. x e. B E. y e. C D = ( x F y ) ) )

Proof

Step Hyp Ref Expression
1 fvelimab 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( D e. ( F " ( B X. C ) ) <-> E. z e. ( B X. C ) ( F ` z ) = D ) )
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 eqeq1d 
 |-  ( z = <. x , y >. -> ( ( F ` z ) = D <-> ( x F y ) = D ) )
6 eqcom 
 |-  ( ( x F y ) = D <-> D = ( x F y ) )
7 5 6 bitrdi 
 |-  ( z = <. x , y >. -> ( ( F ` z ) = D <-> D = ( x F y ) ) )
8 7 rexxp 
 |-  ( E. z e. ( B X. C ) ( F ` z ) = D <-> E. x e. B E. y e. C D = ( x F y ) )
9 1 8 bitrdi 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( D e. ( F " ( B X. C ) ) <-> E. x e. B E. y e. C D = ( x F y ) ) )