Theorem fndmdifcom

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

	Ref	Expression
Assertion	fndmdifcom	$$⊢\left(FFnA\wedge GFnA\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)\leftrightarrow 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(FFnA\wedge GFnA\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(GFnA\wedge FFnA\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(FFnA\wedge GFnA\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(FFnA\wedge GFnA\right)\to \mathrm{dom}\left(F\setminus G\right)=\mathrm{dom}\left(G\setminus F\right)$$