Theorem fndm

Description: The domain of a function. (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	fndm	$$⊢FFnA\to \mathrm{dom}F=A$$

Proof

Step	Hyp	Ref	Expression
1		df-fn	$$⊢FFnA\leftrightarrow \left(\mathrm{Fun}F\wedge \mathrm{dom}F=A\right)$$
2	1	simprbi	$$⊢FFnA\to \mathrm{dom}F=A$$