This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐹 ∩ 𝐺 ) = 𝐴 ) )