Theorem fndmexd

Description: If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024)

	Ref	Expression
Hypotheses	fndmexd.1	$$⊢\phi \to F\in V$$
	fndmexd.2	$$⊢\phi \to FFnD$$
Assertion	fndmexd	$$⊢\phi \to D\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fndmexd.1	$$⊢\phi \to F\in V$$
2		fndmexd.2	$$⊢\phi \to FFnD$$
3	2	fndmd	$$⊢\phi \to \mathrm{dom}F=D$$
4	1	dmexd	$$⊢\phi \to \mathrm{dom}F\in \mathrm{V}$$
5	3 4	eqeltrrd	$$⊢\phi \to D\in \mathrm{V}$$