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

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2	1	eqeq1d	$$⊢\left(FFnA\wedge GFnA\right)\to \left(\mathrm{dom}\left(F\setminus G\right)=\varnothing \leftrightarrow \left\{x\in A|F\left(x\right)\ne G\left(x\right)\right\}=\varnothing \right)$$
3		rabeq0	$$⊢\left\{x\in A|F\left(x\right)\ne G\left(x\right)\right\}=\varnothing \leftrightarrow \forall x\in A\neg F\left(x\right)\ne G\left(x\right)$$
4		nne	$$⊢\neg F\left(x\right)\ne G\left(x\right)\leftrightarrow F\left(x\right)=G\left(x\right)$$
5	4	ralbii	$$⊢\forall x\in A\neg F\left(x\right)\ne G\left(x\right)\leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)$$
6	3 5	bitri	$$⊢\left\{x\in A|F\left(x\right)\ne G\left(x\right)\right\}=\varnothing \leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)$$
7		eqfnfv	$$⊢\left(FFnA\wedge GFnA\right)\to \left(F=G\leftrightarrow \forall x\in AF\left(x\right)=G\left(x\right)\right)$$
8	6 7	bitr4id	$$⊢\left(FFnA\wedge GFnA\right)\to \left(\left\{x\in A|F\left(x\right)\ne G\left(x\right)\right\}=\varnothing \leftrightarrow F=G\right)$$
9	2 8	bitrd	$$⊢\left(FFnA\wedge GFnA\right)\to \left(\mathrm{dom}\left(F\setminus G\right)=\varnothing \leftrightarrow F=G\right)$$