Theorem fndmexd 7840

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 6592	. 2 ⊢ (𝜑 → dom 𝐹 = 𝐷)
3		fndmexd.1	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
4	3	dmexd 7839	. 2 ⊢ (𝜑 → dom 𝐹 ∈ V)
5	2, 4	eqeltrrd 2832	1 ⊢ (𝜑 → 𝐷 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  dom cdm 5619   Fn wfn 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-cnv 5627  df-dm 5629  df-rn 5630  df-fn 6490

This theorem is referenced by:  fndmexb  7842  fsetdmprc0  8785  finnzfsuppd  9263  psrbagfsupp  21862  psrbaglecl  21866  psrbagaddcl  21867  psrbagcon  21868  psrbagleadd1  21871  psrbagconf1o  21872  gsumbagdiaglem  21873  psrass1lem  21875  psrbagev1  22018  psrbagev2  22019  tdeglem1  25996  tdeglem3  25997  tdeglem4  25998  gsumhashmul  33048  mhphf  42696