Theorem fndmexd 7874

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

Hypotheses

Ref	Expression
fndmexd.1	⊢ (𝜑 → 𝐹 ∈ 𝑉)
fndmexd.2	⊢ (𝜑 → 𝐹 Fn 𝐷)

Assertion

Ref	Expression
fndmexd	⊢ (𝜑 → 𝐷 ∈ V)

Proof of Theorem fndmexd

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

Syntax hints:   → wi 4   ∈ wcel 2136  Vcvv 3448  dom cdm 5640   Fn wfn 6505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-sep 5240  ax-pr 5384  ax-un 7707

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-cnv 5648  df-dm 5650  df-rn 5651  df-fn 6513

This theorem is referenced by:  fndmexb  7876  fsetdmprc0  8825  finnzfsuppd  9309  psrbagfsupp  21944  psrbaglecl  21948  psrbagaddcl  21949  psrbagcon  21950  psrbagleadd1  21953  psrbagconf1o  21954  gsumbagdiaglem  21956  psrass1lem  21958  psrbagev1  22103  psrbagev2  22104  tdeglem1  26091  tdeglem3  26092  tdeglem4  26093  gsumhashmul  33201  mhphf  43127