Theorem fexd 7232

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is used by:  mptcnfimad  7989  fidmfisupp  9339  fdmfisuppfi  9341  fsuppco2  9370  fsuppcor  9371  ixpiunwdom  9559  cnfcom3clem  9681  fin23lem32  10343  hasheqf1od  14407  hashf1lem1  14510  fz1isolem  14516  ramval  17090  imasval  17587  imasle  17599  pwsco1mhm  18928  efgtf  19836  gsumval3a  20017  gsumval3lem1  20019  gsumval3lem2  20020  gsumval3  20021  gsumzres  20023  gsumzf1o  20026  gsumzaddlem  20035  gsumzadd  20036  gsumzmhm  20051  gsumzoppg  20058  gsumpt  20076  gsum2dlem2  20085  prdslmodd  21140  dsmmsubg  21943  dsmmlss  21944  islindf2  22014  f1lindf  22022  islindf4  22038  gsumply1subr  22443  txcn  23834  prdstps  23837  qtopval2  23904  fmval  24151  tsmsres  24352  tsmsadd  24355  jensen  27204  fisuppov1  33099  pwrssmgc  33384  gsumpart  33447  gsumwrd2dccat  33462  ply1degltdimlem  34076  ofcfval4  34559  omsfval  34749  omssubadd  34755  carsgval  34758  sseqval  34843  hgt750lemg  35106  filnetlem4  36949  bj-finsumval0  37986  isrngod  38607  isgrpda  38664  iscringd  38707  sticksstones8  42978  limsupre  46413  limsupval3  46464  limsuppnfdlem  46473  limsupvaluz  46480  limsuppnflem  46482  limsupre2lem  46496  climuzlem  46515  climisp  46518  climxrrelem  46521  climxrre  46522  liminfval5  46537  limsupgtlem  46549  liminfvalxr  46555  liminflelimsupuz  46557  liminfgelimsupuz  46560  liminflimsupclim  46579  liminflbuz2  46587  xlimclim2lem  46611  climxlim2  46618  fourierdlem71  46949  fourierdlem80  46958  sge0val  47138  sge0f1o  47154  isomennd  47303  nsssmfmbflem  47550  isuspgrim  48719  isubgr3stgrlem3  48791  isubgr3stgrlem5  48793  clnbgr3stgrgrlim  48842  itcovalendof  49506  thinccisod  50289