Metamath Proof Explorer

Theorem eqfnov

Description: Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005)

Ref Expression
Assertion eqfnov 
|- ( ( F Fn ( A X. B ) /\ G Fn ( C X. D ) ) -> ( F = G <-> ( ( A X. B ) = ( C X. D ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) ) )

Proof

Step Hyp Ref Expression
1 eqfnfv2 
 |-  ( ( F Fn ( A X. B ) /\ G Fn ( C X. D ) ) -> ( F = G <-> ( ( A X. B ) = ( C X. D ) /\ A. z e. ( A X. B ) ( F ` z ) = ( G ` z ) ) ) )
2 fveq2 
 |-  ( z = <. x , y >. -> ( F ` z ) = ( F ` <. x , y >. ) )
3 fveq2 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( G ` <. x , y >. ) )
4 2 3 eqeq12d 
 |-  ( z = <. x , y >. -> ( ( F ` z ) = ( G ` z ) <-> ( F ` <. x , y >. ) = ( G ` <. x , y >. ) ) )
5 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
6 df-ov 
 |-  ( x G y ) = ( G ` <. x , y >. )
7 5 6 eqeq12i 
 |-  ( ( x F y ) = ( x G y ) <-> ( F ` <. x , y >. ) = ( G ` <. x , y >. ) )
8 4 7 bitr4di 
 |-  ( z = <. x , y >. -> ( ( F ` z ) = ( G ` z ) <-> ( x F y ) = ( x G y ) ) )
9 8 ralxp 
 |-  ( A. z e. ( A X. B ) ( F ` z ) = ( G ` z ) <-> A. x e. A A. y e. B ( x F y ) = ( x G y ) )
10 9 anbi2i 
 |-  ( ( ( A X. B ) = ( C X. D ) /\ A. z e. ( A X. B ) ( F ` z ) = ( G ` z ) ) <-> ( ( A X. B ) = ( C X. D ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) )
11 1 10 bitrdi 
 |-  ( ( F Fn ( A X. B ) /\ G Fn ( C X. D ) ) -> ( F = G <-> ( ( A X. B ) = ( C X. D ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) ) )