# Metamath Proof Explorer

## Theorem fndmdifcom

Description: The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015)

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

### Proof

Step Hyp Ref Expression
1 necom ${⊢}{F}\left({x}\right)\ne {G}\left({x}\right)↔{G}\left({x}\right)\ne {F}\left({x}\right)$
2 1 rabbii ${⊢}\left\{{x}\in {A}|{F}\left({x}\right)\ne {G}\left({x}\right)\right\}=\left\{{x}\in {A}|{G}\left({x}\right)\ne {F}\left({x}\right)\right\}$
3 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\}$
4 fndmdif ${⊢}\left({G}Fn{A}\wedge {F}Fn{A}\right)\to \mathrm{dom}\left({G}\setminus {F}\right)=\left\{{x}\in {A}|{G}\left({x}\right)\ne {F}\left({x}\right)\right\}$
5 4 ancoms ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \mathrm{dom}\left({G}\setminus {F}\right)=\left\{{x}\in {A}|{G}\left({x}\right)\ne {F}\left({x}\right)\right\}$
6 2 3 5 3eqtr4a ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \mathrm{dom}\left({F}\setminus {G}\right)=\mathrm{dom}\left({G}\setminus {F}\right)$