Theorem fndmu

Description: A function has a unique domain. (Contributed by NM, 11-Aug-1994)

	Ref	Expression
Assertion	fndmu	$$⊢\left(FFnA\wedge FFnB\right)\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		fndm	$$⊢FFnA\to \mathrm{dom}F=A$$
2		fndm	$$⊢FFnB\to \mathrm{dom}F=B$$
3	1 2	sylan9req	$$⊢\left(FFnA\wedge FFnB\right)\to A=B$$