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

Metamath Proof Explorer

Theorem eqfnfv2

Description: Equality of functions is determined by their values. Exercise 4 of TakeutiZaring p. 28. (Contributed by NM, 3-Aug-1994) (Revised by Mario Carneiro, 31-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 dmeq 
 |-  ( F = G -> dom F = dom G )
2 fndm 
 |-  ( F Fn A -> dom F = A )
3 fndm 
 |-  ( G Fn B -> dom G = B )
4 2 3 eqeqan12d 
 |-  ( ( F Fn A /\ G Fn B ) -> ( dom F = dom G <-> A = B ) )
5 1 4 imbitrid 
 |-  ( ( F Fn A /\ G Fn B ) -> ( F = G -> A = B ) )
6 5 pm4.71rd 
 |-  ( ( F Fn A /\ G Fn B ) -> ( F = G <-> ( A = B /\ F = G ) ) )
7 fneq2 
 |-  ( A = B -> ( G Fn A <-> G Fn B ) )
8 7 biimparc 
 |-  ( ( G Fn B /\ A = B ) -> G Fn A )
9 eqfnfv 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
10 8 9 sylan2 
 |-  ( ( F Fn A /\ ( G Fn B /\ A = B ) ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
11 10 anassrs 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ A = B ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
12 11 pm5.32da 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( A = B /\ F = G ) <-> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) ) )
13 6 12 bitrd 
 |-  ( ( F Fn A /\ G Fn B ) -> ( F = G <-> ( A = B /\ A. x e. A ( F ` x ) = ( G ` x ) ) ) )