Metamath Proof Explorer

Theorem fnov

Description: Representation of a function in terms of its values. (Contributed by NM, 7-Feb-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion fnov 
|- ( F Fn ( A X. B ) <-> F = ( x e. A , y e. B |-> ( x F y ) ) )

Proof

Step Hyp Ref Expression
1 dffn5 
 |-  ( F Fn ( A X. B ) <-> F = ( z e. ( A X. B ) |-> ( F ` z ) ) )
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 mpompt 
 |-  ( z e. ( A X. B ) |-> ( F ` z ) ) = ( x e. A , y e. B |-> ( x F y ) )
6 5 eqeq2i 
 |-  ( F = ( z e. ( A X. B ) |-> ( F ` z ) ) <-> F = ( x e. A , y e. B |-> ( x F y ) ) )
7 1 6 bitri 
 |-  ( F Fn ( A X. B ) <-> F = ( x e. A , y e. B |-> ( x F y ) ) )