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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	fndmexd.2	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
Assertion	fndmexd	⊢ ( 𝜑 → 𝐷 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fndmexd.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		fndmexd.2	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
3	2	fndmd	⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
4	1	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
5	3 4	eqeltrrd	⊢ ( 𝜑 → 𝐷 ∈ V )