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	|- ( ph -> F e. V )
	fndmexd.2	|- ( ph -> F Fn D )
Assertion	fndmexd	|- ( ph -> D e. _V )

Proof

Step	Hyp	Ref	Expression
1		fndmexd.1	|- ( ph -> F e. V )
2		fndmexd.2	|- ( ph -> F Fn D )
3	2	fndmd	|- ( ph -> dom F = D )
4	1	dmexd	|- ( ph -> dom F e. _V )
5	3 4	eqeltrrd	|- ( ph -> D e. _V )