This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqfnov2

Description: Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010)

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

Proof

Step Hyp Ref Expression
1 eqfnov 
 |-  ( ( F Fn ( A X. B ) /\ G Fn ( A X. B ) ) -> ( F = G <-> ( ( A X. B ) = ( A X. B ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) ) )
2 simpr 
 |-  ( ( ( A X. B ) = ( A X. B ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) -> A. x e. A A. y e. B ( x F y ) = ( x G y ) )
3 eqidd 
 |-  ( A. x e. A A. y e. B ( x F y ) = ( x G y ) -> ( A X. B ) = ( A X. B ) )
4 3 ancri 
 |-  ( A. x e. A A. y e. B ( x F y ) = ( x G y ) -> ( ( A X. B ) = ( A X. B ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) )
5 2 4 impbii 
 |-  ( ( ( A X. B ) = ( A X. B ) /\ A. x e. A A. y e. B ( x F y ) = ( x G y ) ) <-> A. x e. A A. y e. B ( x F y ) = ( x G y ) )
6 1 5 bitrdi 
 |-  ( ( F Fn ( A X. B ) /\ G Fn ( A X. B ) ) -> ( F = G <-> A. x e. A A. y e. B ( x F y ) = ( x G y ) ) )