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
|- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A C_ dom ( F i^i G ) ) )

Proof

Step Hyp Ref Expression
1 fneqeql
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> dom ( F i^i G ) = A ) )
2 eqss
 |-  ( dom ( F i^i G ) = A <-> ( dom ( F i^i G ) C_ A /\ A C_ dom ( F i^i G ) ) )
3 inss1
 |-  ( F i^i G ) C_ F
4 dmss
 |-  ( ( F i^i G ) C_ F -> dom ( F i^i G ) C_ dom F )
5 3 4 ax-mp
 |-  dom ( F i^i G ) C_ dom F
6 fndm
 |-  ( F Fn A -> dom F = A )
7 6 adantr
 |-  ( ( F Fn A /\ G Fn A ) -> dom F = A )
8 5 7 sseqtrid
 |-  ( ( F Fn A /\ G Fn A ) -> dom ( F i^i G ) C_ A )
9 8 biantrurd
 |-  ( ( F Fn A /\ G Fn A ) -> ( A C_ dom ( F i^i G ) <-> ( dom ( F i^i G ) C_ A /\ A C_ dom ( F i^i G ) ) ) )
10 2 9 bitr4id
 |-  ( ( F Fn A /\ G Fn A ) -> ( dom ( F i^i G ) = A <-> A C_ dom ( F i^i G ) ) )
11 1 10 bitrd
 |-  ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A C_ dom ( F i^i G ) ) )