Theorem fexd 7173

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 7172	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440  ⟶wf 6488

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  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  7930  fidmfisupp  9275  fdmfisuppfi  9277  fsuppco2  9306  fsuppcor  9307  ixpiunwdom  9495  cnfcom3clem  9614  fin23lem32  10254  hasheqf1od  14276  hashf1lem1  14378  fz1isolem  14384  ramval  16936  imasval  17432  imasle  17444  pwsco1mhm  18757  efgtf  19651  gsumval3a  19832  gsumval3lem1  19834  gsumval3lem2  19835  gsumval3  19836  gsumzres  19838  gsumzf1o  19841  gsumzaddlem  19850  gsumzadd  19851  gsumzmhm  19866  gsumzoppg  19873  gsumpt  19891  gsum2dlem2  19900  prdslmodd  20920  dsmmsubg  21698  dsmmlss  21699  islindf2  21769  f1lindf  21777  islindf4  21793  gsumply1subr  22174  txcn  23570  prdstps  23573  qtopval2  23640  fmval  23887  tsmsres  24088  tsmsadd  24091  jensen  26955  fisuppov1  32762  pwrssmgc  33082  gsumpart  33146  gsumwrd2dccat  33160  ply1degltdimlem  33779  ofcfval4  34262  omsfval  34451  omssubadd  34457  carsgval  34460  sseqval  34545  hgt750lemg  34811  filnetlem4  36575  bj-finsumval0  37490  isrngod  38099  isgrpda  38156  iscringd  38199  sticksstones8  42407  limsupre  45885  limsupval3  45936  limsuppnfdlem  45945  limsupvaluz  45952  limsuppnflem  45954  limsupre2lem  45968  climuzlem  45987  climisp  45990  climxrrelem  45993  climxrre  45994  liminfval5  46009  limsupgtlem  46021  liminfvalxr  46027  liminflelimsupuz  46029  liminfgelimsupuz  46032  liminflimsupclim  46051  liminflbuz2  46059  xlimclim2lem  46083  climxlim2  46090  fourierdlem71  46421  fourierdlem80  46430  sge0val  46610  sge0f1o  46626  isomennd  46775  nsssmfmbflem  47022  isuspgrim  48142  isubgr3stgrlem3  48214  isubgr3stgrlem5  48216  clnbgr3stgrgrlim  48265  itcovalendof  48915  thinccisod  49699