Theorem fndmexd 7799

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3440  dom cdm 5607   Fn wfn 6460

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366  ax-un 7629

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-cnv 5615  df-dm 5617  df-rn 5618  df-fn 6468

This theorem is referenced by:  fndmexb  7801  fsetdmprc0  8692  psrbagfsupp  21203  psrbaglecl  21209  psrbagaddcl  21211  psrbagcon  21213  psrbagconf1o  21219  gsumbagdiaglem  21224  psrass1lem  21226  psrbagev1  21365  psrbagev2  21367  tdeglem1  25300  tdeglem3  25302  tdeglem4  25304  gsumhashmul  31447  finnzfsuppd  42059