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