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

Proof

Step	Hyp	Ref	Expression
1		eqfnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
2		eqcom	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } = 𝐴 ↔ 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } )
3		rabid2	⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
4	2 3	bitri	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
5	1 4	bitr4di	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } = 𝐴 ) )
6		fndmin	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } )
7	6	eqeq1d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( dom ( 𝐹 ∩ 𝐺 ) = 𝐴 ↔ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } = 𝐴 ) )
8	5 7	bitr4d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ dom ( 𝐹 ∩ 𝐺 ) = 𝐴 ) )