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

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 ) )