Theorem fndmexd 7848

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 7847	. 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 7682

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  7850  fsetdmprc0  8796  finnzfsuppd  9280  psrbagfsupp  21879  psrbaglecl  21883  psrbagaddcl  21884  psrbagcon  21885  psrbagleadd1  21888  psrbagconf1o  21889  gsumbagdiaglem  21890  psrass1lem  21892  psrbagev1  22036  psrbagev2  22037  tdeglem1  26023  tdeglem3  26024  tdeglem4  26025  gsumhashmul  33131  mhphf  42876