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

Metamath Proof Explorer

Theorem eqfnfv2f

Description: Equality of functions is determined by their values. Special case of Exercise 4 of TakeutiZaring p. 28 (with domain equality omitted). This version of eqfnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004)

Ref Expression
Hypotheses eqfnfv2f.1 
|- F/_ x F
eqfnfv2f.2 
|- F/_ x G
Assertion eqfnfv2f 
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )

Proof

Step Hyp Ref Expression
1 eqfnfv2f.1 
 |-  F/_ x F
2 eqfnfv2f.2 
 |-  F/_ x G
3 eqfnfv 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. z e. A ( F ` z ) = ( G ` z ) ) )
4 nfcv 
 |-  F/_ x z
5 1 4 nffv 
 |-  F/_ x ( F ` z )
6 2 4 nffv 
 |-  F/_ x ( G ` z )
7 5 6 nfeq 
 |-  F/ x ( F ` z ) = ( G ` z )
8 nfv 
 |-  F/ z ( F ` x ) = ( G ` x )
9 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
10 fveq2 
 |-  ( z = x -> ( G ` z ) = ( G ` x ) )
11 9 10 eqeq12d 
 |-  ( z = x -> ( ( F ` z ) = ( G ` z ) <-> ( F ` x ) = ( G ` x ) ) )
12 7 8 11 cbvralw 
 |-  ( A. z e. A ( F ` z ) = ( G ` z ) <-> A. x e. A ( F ` x ) = ( G ` x ) )
13 3 12 bitrdi 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )