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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnssres	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑋 ) Fn 𝑋 )
2	1	3adant2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑋 ) Fn 𝑋 )
3		fnssres	⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐺 ↾ 𝑋 ) Fn 𝑋 )
4	3	3adant1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐺 ↾ 𝑋 ) Fn 𝑋 )
5		fneqeql	⊢ ( ( ( 𝐹 ↾ 𝑋 ) Fn 𝑋 ∧ ( 𝐺 ↾ 𝑋 ) Fn 𝑋 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ) )
6	2 4 5	syl2anc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ) )
7		resindir	⊢ ( ( 𝐹 ∩ 𝐺 ) ↾ 𝑋 ) = ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) )
8	7	dmeqi	⊢ dom ( ( 𝐹 ∩ 𝐺 ) ↾ 𝑋 ) = dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) )
9		dmres	⊢ dom ( ( 𝐹 ∩ 𝐺 ) ↾ 𝑋 ) = ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) )
10	8 9	eqtr3i	⊢ dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) )
11	10	eqeq1i	⊢ ( dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ↔ ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) ) = 𝑋 )
12		dfss2	⊢ ( 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) ↔ ( 𝑋 ∩ dom ( 𝐹 ∩ 𝐺 ) ) = 𝑋 )
13	11 12	bitr4i	⊢ ( dom ( ( 𝐹 ↾ 𝑋 ) ∩ ( 𝐺 ↾ 𝑋 ) ) = 𝑋 ↔ 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) )
14	6 13	bitrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )