Theorem fndmexd 7849

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  dom cdm 5625   Fn wfn 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-cnv 5633  df-dm 5635  df-rn 5636  df-fn 6496

This theorem is referenced by:  fndmexb  7851  fsetdmprc0  8797  finnzfsuppd  9281  psrbagfsupp  21880  psrbaglecl  21884  psrbagaddcl  21885  psrbagcon  21886  psrbagleadd1  21889  psrbagconf1o  21890  gsumbagdiaglem  21891  psrass1lem  21893  psrbagev1  22037  psrbagev2  22038  tdeglem1  26024  tdeglem3  26025  tdeglem4  26026  gsumhashmul  33153  mhphf  42918