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 3430  ⟶wf 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-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5370

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 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500

This theorem is referenced by:  mptcnfimad  7932  fidmfisupp  9278  fdmfisuppfi  9280  fsuppco2  9309  fsuppcor  9310  ixpiunwdom  9498  cnfcom3clem  9617  fin23lem32  10257  hasheqf1od  14306  hashf1lem1  14408  fz1isolem  14414  ramval  16970  imasval  17466  imasle  17478  pwsco1mhm  18791  efgtf  19688  gsumval3a  19869  gsumval3lem1  19871  gsumval3lem2  19872  gsumval3  19873  gsumzres  19875  gsumzf1o  19878  gsumzaddlem  19887  gsumzadd  19888  gsumzmhm  19903  gsumzoppg  19910  gsumpt  19928  gsum2dlem2  19937  prdslmodd  20955  dsmmsubg  21733  dsmmlss  21734  islindf2  21804  f1lindf  21812  islindf4  21828  gsumply1subr  22207  txcn  23601  prdstps  23604  qtopval2  23671  fmval  23918  tsmsres  24119  tsmsadd  24122  jensen  26966  fisuppov1  32771  pwrssmgc  33075  gsumpart  33139  gsumwrd2dccat  33154  ply1degltdimlem  33782  ofcfval4  34265  omsfval  34454  omssubadd  34460  carsgval  34463  sseqval  34548  hgt750lemg  34814  filnetlem4  36579  bj-finsumval0  37615  isrngod  38233  isgrpda  38290  iscringd  38333  sticksstones8  42606  limsupre  46087  limsupval3  46138  limsuppnfdlem  46147  limsupvaluz  46154  limsuppnflem  46156  limsupre2lem  46170  climuzlem  46189  climisp  46192  climxrrelem  46195  climxrre  46196  liminfval5  46211  limsupgtlem  46223  liminfvalxr  46229  liminflelimsupuz  46231  liminfgelimsupuz  46234  liminflimsupclim  46253  liminflbuz2  46261  xlimclim2lem  46285  climxlim2  46292  fourierdlem71  46623  fourierdlem80  46632  sge0val  46812  sge0f1o  46828  isomennd  46977  nsssmfmbflem  47224  isuspgrim  48384  isubgr3stgrlem3  48456  isubgr3stgrlem5  48458  clnbgr3stgrgrlim  48507  itcovalendof  49157  thinccisod  49941