# Metamath Proof Explorer

## Theorem fndmdifeq0

Description: The difference set of two functions is empty if and only if the functions are equal. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion fndmdifeq0 ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left(\mathrm{dom}\left({F}\setminus {G}\right)=\varnothing ↔{F}={G}\right)$

### Proof

Step Hyp Ref Expression
1 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\}$
2 1 eqeq1d ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left(\mathrm{dom}\left({F}\setminus {G}\right)=\varnothing ↔\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}=\varnothing \right)$
3 eqfnfv ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
4 rabeq0 ${⊢}\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)\ne {G}\left({x}\right)$
5 nne ${⊢}¬{F}\left({x}\right)\ne {G}\left({x}\right)↔{F}\left({x}\right)={G}\left({x}\right)$
6 5 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{F}\left({x}\right)\ne {G}\left({x}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)$
7 4 6 bitri ${⊢}\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)$
8 3 7 syl6rbbr ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left(\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}=\varnothing ↔{F}={G}\right)$
9 2 8 bitrd ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left(\mathrm{dom}\left({F}\setminus {G}\right)=\varnothing ↔{F}={G}\right)$