# Metamath Proof Explorer

## Theorem fndmdif

Description: Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion fndmdif
`|- ( ( F Fn A /\ G Fn A ) -> dom ( F \ G ) = { x e. A | ( F ` x ) =/= ( G ` x ) } )`

### Proof

Step Hyp Ref Expression
1 difss
` |-  ( F \ G ) C_ F`
2 dmss
` |-  ( ( F \ G ) C_ F -> dom ( F \ G ) C_ dom F )`
3 1 2 ax-mp
` |-  dom ( F \ G ) C_ dom F`
4 fndm
` |-  ( F Fn A -> dom F = A )`
` |-  ( ( F Fn A /\ G Fn A ) -> dom F = A )`
6 3 5 sseqtrid
` |-  ( ( F Fn A /\ G Fn A ) -> dom ( F \ G ) C_ A )`
7 sseqin2
` |-  ( dom ( F \ G ) C_ A <-> ( A i^i dom ( F \ G ) ) = dom ( F \ G ) )`
8 6 7 sylib
` |-  ( ( F Fn A /\ G Fn A ) -> ( A i^i dom ( F \ G ) ) = dom ( F \ G ) )`
9 vex
` |-  x e. _V`
10 9 eldm
` |-  ( x e. dom ( F \ G ) <-> E. y x ( F \ G ) y )`
11 eqcom
` |-  ( ( F ` x ) = ( G ` x ) <-> ( G ` x ) = ( F ` x ) )`
12 fnbrfvb
` |-  ( ( G Fn A /\ x e. A ) -> ( ( G ` x ) = ( F ` x ) <-> x G ( F ` x ) ) )`
13 11 12 syl5bb
` |-  ( ( G Fn A /\ x e. A ) -> ( ( F ` x ) = ( G ` x ) <-> x G ( F ` x ) ) )`
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( F ` x ) = ( G ` x ) <-> x G ( F ` x ) ) )`
15 14 necon3abid
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( F ` x ) =/= ( G ` x ) <-> -. x G ( F ` x ) ) )`
16 fvex
` |-  ( F ` x ) e. _V`
17 breq2
` |-  ( y = ( F ` x ) -> ( x G y <-> x G ( F ` x ) ) )`
18 17 notbid
` |-  ( y = ( F ` x ) -> ( -. x G y <-> -. x G ( F ` x ) ) )`
19 16 18 ceqsexv
` |-  ( E. y ( y = ( F ` x ) /\ -. x G y ) <-> -. x G ( F ` x ) )`
20 15 19 syl6bbr
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( F ` x ) =/= ( G ` x ) <-> E. y ( y = ( F ` x ) /\ -. x G y ) ) )`
21 eqcom
` |-  ( y = ( F ` x ) <-> ( F ` x ) = y )`
22 fnbrfvb
` |-  ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )`
23 21 22 syl5bb
` |-  ( ( F Fn A /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )`
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )`
25 24 anbi1d
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( y = ( F ` x ) /\ -. x G y ) <-> ( x F y /\ -. x G y ) ) )`
26 brdif
` |-  ( x ( F \ G ) y <-> ( x F y /\ -. x G y ) )`
27 25 26 syl6bbr
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( ( y = ( F ` x ) /\ -. x G y ) <-> x ( F \ G ) y ) )`
28 27 exbidv
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( E. y ( y = ( F ` x ) /\ -. x G y ) <-> E. y x ( F \ G ) y ) )`
29 20 28 bitr2d
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( E. y x ( F \ G ) y <-> ( F ` x ) =/= ( G ` x ) ) )`
30 10 29 syl5bb
` |-  ( ( ( F Fn A /\ G Fn A ) /\ x e. A ) -> ( x e. dom ( F \ G ) <-> ( F ` x ) =/= ( G ` x ) ) )`
31 30 rabbi2dva
` |-  ( ( F Fn A /\ G Fn A ) -> ( A i^i dom ( F \ G ) ) = { x e. A | ( F ` x ) =/= ( G ` x ) } )`
32 8 31 eqtr3d
` |-  ( ( F Fn A /\ G Fn A ) -> dom ( F \ G ) = { x e. A | ( F ` x ) =/= ( G ` x ) } )`