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 ) ) )