Theorem fexd 7175

Description: If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
fexd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fexd.2	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Assertion

Ref	Expression
fexd	⊢ (𝜑 → 𝐹 ∈ V)

Proof of Theorem fexd

Step	Hyp	Ref	Expression
1		fexd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fexd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
3		fex 7174	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  ⟶wf 6489

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-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pr 5378

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-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  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-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501

This theorem is referenced by:  mptcnfimad  7932  fidmfisupp  9279  fdmfisuppfi  9281  fsuppco2  9310  fsuppcor  9311  ixpiunwdom  9499  cnfcom3clem  9618  fin23lem32  10258  hasheqf1od  14280  hashf1lem1  14382  fz1isolem  14388  ramval  16940  imasval  17436  imasle  17448  pwsco1mhm  18761  efgtf  19655  gsumval3a  19836  gsumval3lem1  19838  gsumval3lem2  19839  gsumval3  19840  gsumzres  19842  gsumzf1o  19845  gsumzaddlem  19854  gsumzadd  19855  gsumzmhm  19870  gsumzoppg  19877  gsumpt  19895  gsum2dlem2  19904  prdslmodd  20924  dsmmsubg  21702  dsmmlss  21703  islindf2  21773  f1lindf  21781  islindf4  21797  gsumply1subr  22178  txcn  23574  prdstps  23577  qtopval2  23644  fmval  23891  tsmsres  24092  tsmsadd  24095  jensen  26959  fisuppov1  32743  pwrssmgc  33063  gsumpart  33127  gsumwrd2dccat  33141  ply1degltdimlem  33760  ofcfval4  34243  omsfval  34432  omssubadd  34438  carsgval  34441  sseqval  34526  hgt750lemg  34792  filnetlem4  36556  bj-finsumval0  37461  isrngod  38070  isgrpda  38127  iscringd  38170  sticksstones8  42444  limsupre  45921  limsupval3  45972  limsuppnfdlem  45981  limsupvaluz  45988  limsuppnflem  45990  limsupre2lem  46004  climuzlem  46023  climisp  46026  climxrrelem  46029  climxrre  46030  liminfval5  46045  limsupgtlem  46057  liminfvalxr  46063  liminflelimsupuz  46065  liminfgelimsupuz  46068  liminflimsupclim  46087  liminflbuz2  46095  xlimclim2lem  46119  climxlim2  46126  fourierdlem71  46457  fourierdlem80  46466  sge0val  46646  sge0f1o  46662  isomennd  46811  nsssmfmbflem  47058  isuspgrim  48178  isubgr3stgrlem3  48250  isubgr3stgrlem5  48252  clnbgr3stgrgrlim  48301  itcovalendof  48951  thinccisod  49735