Theorem fexd 7085

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426

This theorem is referenced by:  fdmfisuppfi  9067  fsuppco2  9092  fsuppcor  9093  ixpiunwdom  9279  cnfcom3clem  9393  fin23lem32  10031  hasheqf1od  13996  hashf1lem1  14096  hashf1lem1OLD  14097  fz1isolem  14103  ramval  16637  imasval  17139  imasle  17151  pwsco1mhm  18385  efgtf  19243  gsumval3a  19419  gsumval3lem1  19421  gsumval3lem2  19422  gsumval3  19423  gsumzres  19425  gsumzf1o  19428  gsumzaddlem  19437  gsumzadd  19438  gsumzmhm  19453  gsumzoppg  19460  gsumpt  19478  gsum2dlem2  19487  prdslmodd  20146  dsmmsubg  20860  dsmmlss  20861  islindf2  20931  f1lindf  20939  islindf4  20955  gsumply1subr  21315  txcn  22685  prdstps  22688  qtopval2  22755  fmval  23002  tsmsres  23203  tsmsadd  23206  jensen  26043  pwrssmgc  31180  gsumpart  31217  ofcfval4  31973  omsfval  32161  omssubadd  32167  carsgval  32170  sseqval  32255  hgt750lemg  32534  filnetlem4  34497  bj-finsumval0  35383  isrngod  35983  isgrpda  36040  iscringd  36083  sticksstones8  40037  fidmfisupp  42628  limsupre  43072  limsupval3  43123  limsuppnfdlem  43132  limsupvaluz  43139  limsuppnflem  43141  limsupre2lem  43155  climuzlem  43174  climisp  43177  climxrrelem  43180  climxrre  43181  liminfval5  43196  limsupgtlem  43208  liminfvalxr  43214  liminflelimsupuz  43216  liminfgelimsupuz  43219  liminflimsupclim  43238  liminflbuz2  43246  xlimclim2lem  43270  climxlim2  43277  fourierdlem71  43608  fourierdlem80  43617  sge0val  43794  sge0f1o  43810  isomennd  43959  nsssmfmbflem  44200  itcovalendof  45903