Theorem fndmexd 7609

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

Syntax hints:   → wi 4   ∈ wcel 2112  Vcvv 3407  dom cdm 5517   Fn wfn 6323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291  ax-un 7452

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3077  df-v 3409  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-br 5026  df-opab 5088  df-cnv 5525  df-dm 5527  df-rn 5528  df-fn 6331

This theorem is referenced by:  fndmexb  7611  fsetdmprc0  8435  psrbagfsupp  20667  psrbaglecl  20673  psrbagaddcl  20675  psrbagcon  20677  psrbagconf1o  20683  gsumbagdiaglem  20688  psrass1lem  20690  psrbagev1  20823  psrbagev2  20825  tdeglem1  24740  tdeglem3  24742  tdeglem4  24744  gsumhashmul  30827  finnzfsuppd  41273