# 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 ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \mathrm{dom}\left({F}\setminus {G}\right)=\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 difss ${⊢}{F}\setminus {G}\subseteq {F}$
2 dmss ${⊢}{F}\setminus {G}\subseteq {F}\to \mathrm{dom}\left({F}\setminus {G}\right)\subseteq \mathrm{dom}{F}$
3 1 2 ax-mp ${⊢}\mathrm{dom}\left({F}\setminus {G}\right)\subseteq \mathrm{dom}{F}$
4 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
5 4 adantr ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \mathrm{dom}{F}={A}$
6 3 5 sseqtrid ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \mathrm{dom}\left({F}\setminus {G}\right)\subseteq {A}$
7 sseqin2 ${⊢}\mathrm{dom}\left({F}\setminus {G}\right)\subseteq {A}↔{A}\cap \mathrm{dom}\left({F}\setminus {G}\right)=\mathrm{dom}\left({F}\setminus {G}\right)$
8 6 7 sylib ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to {A}\cap \mathrm{dom}\left({F}\setminus {G}\right)=\mathrm{dom}\left({F}\setminus {G}\right)$
9 vex ${⊢}{x}\in \mathrm{V}$
10 9 eldm ${⊢}{x}\in \mathrm{dom}\left({F}\setminus {G}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}{x}\left({F}\setminus {G}\right){y}$
11 eqcom ${⊢}{F}\left({x}\right)={G}\left({x}\right)↔{G}\left({x}\right)={F}\left({x}\right)$
12 fnbrfvb ${⊢}\left({G}Fn{A}\wedge {x}\in {A}\right)\to \left({G}\left({x}\right)={F}\left({x}\right)↔{x}{G}{F}\left({x}\right)\right)$
13 11 12 syl5bb ${⊢}\left({G}Fn{A}\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={G}\left({x}\right)↔{x}{G}{F}\left({x}\right)\right)$
14 13 adantll ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={G}\left({x}\right)↔{x}{G}{F}\left({x}\right)\right)$
15 14 necon3abid ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)\ne {G}\left({x}\right)↔¬{x}{G}{F}\left({x}\right)\right)$
16 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
17 breq2 ${⊢}{y}={F}\left({x}\right)\to \left({x}{G}{y}↔{x}{G}{F}\left({x}\right)\right)$
18 17 notbid ${⊢}{y}={F}\left({x}\right)\to \left(¬{x}{G}{y}↔¬{x}{G}{F}\left({x}\right)\right)$
19 16 18 ceqsexv ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\wedge ¬{x}{G}{y}\right)↔¬{x}{G}{F}\left({x}\right)$
20 15 19 syl6bbr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)\ne {G}\left({x}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\wedge ¬{x}{G}{y}\right)\right)$
21 eqcom ${⊢}{y}={F}\left({x}\right)↔{F}\left({x}\right)={y}$
22 fnbrfvb ${⊢}\left({F}Fn{A}\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={y}↔{x}{F}{y}\right)$
23 21 22 syl5bb ${⊢}\left({F}Fn{A}\wedge {x}\in {A}\right)\to \left({y}={F}\left({x}\right)↔{x}{F}{y}\right)$
24 23 adantlr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left({y}={F}\left({x}\right)↔{x}{F}{y}\right)$
25 24 anbi1d ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left(\left({y}={F}\left({x}\right)\wedge ¬{x}{G}{y}\right)↔\left({x}{F}{y}\wedge ¬{x}{G}{y}\right)\right)$
26 brdif ${⊢}{x}\left({F}\setminus {G}\right){y}↔\left({x}{F}{y}\wedge ¬{x}{G}{y}\right)$
27 25 26 syl6bbr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left(\left({y}={F}\left({x}\right)\wedge ¬{x}{G}{y}\right)↔{x}\left({F}\setminus {G}\right){y}\right)$
28 27 exbidv ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={F}\left({x}\right)\wedge ¬{x}{G}{y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}{x}\left({F}\setminus {G}\right){y}\right)$
29 20 28 bitr2d ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{x}\left({F}\setminus {G}\right){y}↔{F}\left({x}\right)\ne {G}\left({x}\right)\right)$
30 10 29 syl5bb ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {x}\in {A}\right)\to \left({x}\in \mathrm{dom}\left({F}\setminus {G}\right)↔{F}\left({x}\right)\ne {G}\left({x}\right)\right)$
31 30 rabbi2dva ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to {A}\cap \mathrm{dom}\left({F}\setminus {G}\right)=\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}$
32 8 31 eqtr3d ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \mathrm{dom}\left({F}\setminus {G}\right)=\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}$