Theorem fnreseql

Description: Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	fnreseql	|- ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( ( F |` X ) = ( G |` X ) <-> X C_ dom ( F i^i G ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnssres	|- ( ( F Fn A /\ X C_ A ) -> ( F |` X ) Fn X )
2	1	3adant2	|- ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( F |` X ) Fn X )
3		fnssres	|- ( ( G Fn A /\ X C_ A ) -> ( G |` X ) Fn X )
4	3	3adant1	|- ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( G |` X ) Fn X )
5		fneqeql	|- ( ( ( F |` X ) Fn X /\ ( G |` X ) Fn X ) -> ( ( F |` X ) = ( G |` X ) <-> dom ( ( F |` X ) i^i ( G |` X ) ) = X ) )
6	2 4 5	syl2anc	|- ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( ( F |` X ) = ( G |` X ) <-> dom ( ( F |` X ) i^i ( G |` X ) ) = X ) )
7		resindir	|- ( ( F i^i G ) |` X ) = ( ( F |` X ) i^i ( G |` X ) )
8	7	dmeqi	|- dom ( ( F i^i G ) |` X ) = dom ( ( F |` X ) i^i ( G |` X ) )
9		dmres	|- dom ( ( F i^i G ) |` X ) = ( X i^i dom ( F i^i G ) )
10	8 9	eqtr3i	|- dom ( ( F |` X ) i^i ( G |` X ) ) = ( X i^i dom ( F i^i G ) )
11	10	eqeq1i	|- ( dom ( ( F |` X ) i^i ( G |` X ) ) = X <-> ( X i^i dom ( F i^i G ) ) = X )
12		df-ss	|- ( X C_ dom ( F i^i G ) <-> ( X i^i dom ( F i^i G ) ) = X )
13	11 12	bitr4i	|- ( dom ( ( F |` X ) i^i ( G |` X ) ) = X <-> X C_ dom ( F i^i G ) )
14	6 13	bitrdi	|- ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( ( F |` X ) = ( G |` X ) <-> X C_ dom ( F i^i G ) ) )