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