Theorem fexd 7163

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436  ⟶wf 6478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490

This theorem is referenced by:  mptcnfimad  7921  fidmfisupp  9262  fdmfisuppfi  9264  fsuppco2  9293  fsuppcor  9294  ixpiunwdom  9482  cnfcom3clem  9601  fin23lem32  10238  hasheqf1od  14260  hashf1lem1  14362  fz1isolem  14368  ramval  16920  imasval  17415  imasle  17427  pwsco1mhm  18706  efgtf  19601  gsumval3a  19782  gsumval3lem1  19784  gsumval3lem2  19785  gsumval3  19786  gsumzres  19788  gsumzf1o  19791  gsumzaddlem  19800  gsumzadd  19801  gsumzmhm  19816  gsumzoppg  19823  gsumpt  19841  gsum2dlem2  19850  prdslmodd  20872  dsmmsubg  21650  dsmmlss  21651  islindf2  21721  f1lindf  21729  islindf4  21745  gsumply1subr  22116  txcn  23511  prdstps  23514  qtopval2  23581  fmval  23828  tsmsres  24029  tsmsadd  24032  jensen  26897  fisuppov1  32625  pwrssmgc  32942  gsumpart  33010  gsumwrd2dccat  33020  ply1degltdimlem  33589  ofcfval4  34072  omsfval  34262  omssubadd  34268  carsgval  34271  sseqval  34356  hgt750lemg  34622  filnetlem4  36355  bj-finsumval0  37259  isrngod  37878  isgrpda  37935  iscringd  37978  sticksstones8  42126  limsupre  45622  limsupval3  45673  limsuppnfdlem  45682  limsupvaluz  45689  limsuppnflem  45691  limsupre2lem  45705  climuzlem  45724  climisp  45727  climxrrelem  45730  climxrre  45731  liminfval5  45746  limsupgtlem  45758  liminfvalxr  45764  liminflelimsupuz  45766  liminfgelimsupuz  45769  liminflimsupclim  45788  liminflbuz2  45796  xlimclim2lem  45820  climxlim2  45827  fourierdlem71  46158  fourierdlem80  46167  sge0val  46347  sge0f1o  46363  isomennd  46512  nsssmfmbflem  46759  isuspgrim  47880  isubgr3stgrlem3  47952  isubgr3stgrlem5  47954  clnbgr3stgrgrlim  48003  itcovalendof  48654  thinccisod  49439