Theorem fexd 7171

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438  ⟶wf 6486

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 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498

This theorem is referenced by:  mptcnfimad  7928  fidmfisupp  9273  fdmfisuppfi  9275  fsuppco2  9304  fsuppcor  9305  ixpiunwdom  9493  cnfcom3clem  9612  fin23lem32  10252  hasheqf1od  14274  hashf1lem1  14376  fz1isolem  14382  ramval  16934  imasval  17430  imasle  17442  pwsco1mhm  18755  efgtf  19649  gsumval3a  19830  gsumval3lem1  19832  gsumval3lem2  19833  gsumval3  19834  gsumzres  19836  gsumzf1o  19839  gsumzaddlem  19848  gsumzadd  19849  gsumzmhm  19864  gsumzoppg  19871  gsumpt  19889  gsum2dlem2  19898  prdslmodd  20918  dsmmsubg  21696  dsmmlss  21697  islindf2  21767  f1lindf  21775  islindf4  21791  gsumply1subr  22172  txcn  23568  prdstps  23571  qtopval2  23638  fmval  23885  tsmsres  24086  tsmsadd  24089  jensen  26953  fisuppov1  32711  pwrssmgc  33031  gsumpart  33095  gsumwrd2dccat  33109  ply1degltdimlem  33728  ofcfval4  34211  omsfval  34400  omssubadd  34406  carsgval  34409  sseqval  34494  hgt750lemg  34760  filnetlem4  36524  bj-finsumval0  37429  isrngod  38038  isgrpda  38095  iscringd  38138  sticksstones8  42346  limsupre  45827  limsupval3  45878  limsuppnfdlem  45887  limsupvaluz  45894  limsuppnflem  45896  limsupre2lem  45910  climuzlem  45929  climisp  45932  climxrrelem  45935  climxrre  45936  liminfval5  45951  limsupgtlem  45963  liminfvalxr  45969  liminflelimsupuz  45971  liminfgelimsupuz  45974  liminflimsupclim  45993  liminflbuz2  46001  xlimclim2lem  46025  climxlim2  46032  fourierdlem71  46363  fourierdlem80  46372  sge0val  46552  sge0f1o  46568  isomennd  46717  nsssmfmbflem  46964  isuspgrim  48084  isubgr3stgrlem3  48156  isubgr3stgrlem5  48158  clnbgr3stgrgrlim  48207  itcovalendof  48857  thinccisod  49641