Theorem fneqeql2

Description: Two functions are equal iff their equalizer contains the whole domain. (Contributed by Stefan O'Rear, 9-Mar-2015)

	Ref	Expression
Assertion	fneqeql2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fneqeql	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ dom ( 𝐹 ∩ 𝐺 ) = 𝐴 ) )
2		inss1	⊢ ( 𝐹 ∩ 𝐺 ) ⊆ 𝐹
3		dmss	⊢ ( ( 𝐹 ∩ 𝐺 ) ⊆ 𝐹 → dom ( 𝐹 ∩ 𝐺 ) ⊆ dom 𝐹 )
4	2 3	ax-mp	⊢ dom ( 𝐹 ∩ 𝐺 ) ⊆ dom 𝐹
5		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6	5	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom 𝐹 = 𝐴 )
7	4 6	sseqtrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∩ 𝐺 ) ⊆ 𝐴 )
8	7	biantrurd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ↔ ( dom ( 𝐹 ∩ 𝐺 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) ) )
9		eqss	⊢ ( dom ( 𝐹 ∩ 𝐺 ) = 𝐴 ↔ ( dom ( 𝐹 ∩ 𝐺 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
10	8 9	syl6rbbr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( dom ( 𝐹 ∩ 𝐺 ) = 𝐴 ↔ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
11	1 10	bitrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )