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

Metamath Proof Explorer

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