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 FFnAGFnAF=GdomFG=A

Proof

Step Hyp Ref Expression
1 eqfnfv FFnAGFnAF=GxAFx=Gx
2 eqcom xA|Fx=Gx=AA=xA|Fx=Gx
3 rabid2 A=xA|Fx=GxxAFx=Gx
4 2 3 bitri xA|Fx=Gx=AxAFx=Gx
5 1 4 bitr4di FFnAGFnAF=GxA|Fx=Gx=A
6 fndmin FFnAGFnAdomFG=xA|Fx=Gx
7 6 eqeq1d FFnAGFnAdomFG=AxA|Fx=Gx=A
8 5 7 bitr4d FFnAGFnAF=GdomFG=A