Metamath Proof Explorer


Theorem fneqeql

Description: Two functions are equal iff their equalizer is the whole domain. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion fneqeql
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> dom ( F i^i G ) = A ) )

Proof

Step Hyp Ref Expression
1 eqfnfv
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
2 eqcom
 |-  ( { x e. A | ( F ` x ) = ( G ` x ) } = A <-> A = { x e. A | ( F ` x ) = ( G ` x ) } )
3 rabid2
 |-  ( A = { x e. A | ( F ` x ) = ( G ` x ) } <-> A. x e. A ( F ` x ) = ( G ` x ) )
4 2 3 bitri
 |-  ( { x e. A | ( F ` x ) = ( G ` x ) } = A <-> A. x e. A ( F ` x ) = ( G ` x ) )
5 1 4 bitr4di
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> { x e. A | ( F ` x ) = ( G ` x ) } = A ) )
6 fndmin
 |-  ( ( F Fn A /\ G Fn A ) -> dom ( F i^i G ) = { x e. A | ( F ` x ) = ( G ` x ) } )
7 6 eqeq1d
 |-  ( ( F Fn A /\ G Fn A ) -> ( dom ( F i^i G ) = A <-> { x e. A | ( F ` x ) = ( G ` x ) } = A ) )
8 5 7 bitr4d
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> dom ( F i^i G ) = A ) )