Theorem fexd 7156

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436  ⟶wf 6472

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pr 5365

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484

This theorem is referenced by:  mptcnfimad  7913  fidmfisupp  9251  fdmfisuppfi  9253  fsuppco2  9282  fsuppcor  9283  ixpiunwdom  9471  cnfcom3clem  9590  fin23lem32  10230  hasheqf1od  14255  hashf1lem1  14357  fz1isolem  14363  ramval  16915  imasval  17410  imasle  17422  pwsco1mhm  18735  efgtf  19629  gsumval3a  19810  gsumval3lem1  19812  gsumval3lem2  19813  gsumval3  19814  gsumzres  19816  gsumzf1o  19819  gsumzaddlem  19828  gsumzadd  19829  gsumzmhm  19844  gsumzoppg  19851  gsumpt  19869  gsum2dlem2  19878  prdslmodd  20897  dsmmsubg  21675  dsmmlss  21676  islindf2  21746  f1lindf  21754  islindf4  21770  gsumply1subr  22141  txcn  23536  prdstps  23539  qtopval2  23606  fmval  23853  tsmsres  24054  tsmsadd  24057  jensen  26921  fisuppov1  32656  pwrssmgc  32973  gsumpart  33029  gsumwrd2dccat  33039  ply1degltdimlem  33627  ofcfval4  34110  omsfval  34299  omssubadd  34305  carsgval  34308  sseqval  34393  hgt750lemg  34659  filnetlem4  36415  bj-finsumval0  37319  isrngod  37938  isgrpda  37995  iscringd  38038  sticksstones8  42186  limsupre  45679  limsupval3  45730  limsuppnfdlem  45739  limsupvaluz  45746  limsuppnflem  45748  limsupre2lem  45762  climuzlem  45781  climisp  45784  climxrrelem  45787  climxrre  45788  liminfval5  45803  limsupgtlem  45815  liminfvalxr  45821  liminflelimsupuz  45823  liminfgelimsupuz  45826  liminflimsupclim  45845  liminflbuz2  45853  xlimclim2lem  45877  climxlim2  45884  fourierdlem71  46215  fourierdlem80  46224  sge0val  46404  sge0f1o  46420  isomennd  46569  nsssmfmbflem  46816  isuspgrim  47927  isubgr3stgrlem3  47999  isubgr3stgrlem5  48001  clnbgr3stgrgrlim  48050  itcovalendof  48701  thinccisod  49486