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		eqss	⊢ ( dom ( 𝐹 ∩ 𝐺 ) = 𝐴 ↔ ( dom ( 𝐹 ∩ 𝐺 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
3		inss1	⊢ ( 𝐹 ∩ 𝐺 ) ⊆ 𝐹
4		dmss	⊢ ( ( 𝐹 ∩ 𝐺 ) ⊆ 𝐹 → dom ( 𝐹 ∩ 𝐺 ) ⊆ dom 𝐹 )
5	3 4	ax-mp	⊢ dom ( 𝐹 ∩ 𝐺 ) ⊆ dom 𝐹
6		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
7	6	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom 𝐹 = 𝐴 )
8	5 7	sseqtrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∩ 𝐺 ) ⊆ 𝐴 )
9	8	biantrurd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ↔ ( dom ( 𝐹 ∩ 𝐺 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) ) )
10	2 9	bitr4id	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( dom ( 𝐹 ∩ 𝐺 ) = 𝐴 ↔ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )
11	1 10	bitrd	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ 𝐴 ⊆ dom ( 𝐹 ∩ 𝐺 ) ) )