Theorem fexd 7225

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544

This theorem is referenced by:  mptcnfimad  7979  fidmfisupp  9328  fdmfisuppfi  9330  fsuppco2  9359  fsuppcor  9360  ixpiunwdom  9548  cnfcom3clem  9670  fin23lem32  10323  hasheqf1od  14385  hashf1lem1  14488  fz1isolem  14494  ramval  17063  imasval  17560  imasle  17572  pwsco1mhm  18886  efgtf  19787  gsumval3a  19968  gsumval3lem1  19970  gsumval3lem2  19971  gsumval3  19972  gsumzres  19974  gsumzf1o  19977  gsumzaddlem  19986  gsumzadd  19987  gsumzmhm  20002  gsumzoppg  20009  gsumpt  20027  gsum2dlem2  20036  prdslmodd  21090  dsmmsubg  21893  dsmmlss  21894  islindf2  21964  f1lindf  21972  islindf4  21988  gsumply1subr  22393  txcn  23783  prdstps  23786  qtopval2  23853  fmval  24100  tsmsres  24301  tsmsadd  24304  jensen  27153  fisuppov1  33028  pwrssmgc  33320  gsumpart  33383  gsumwrd2dccat  33398  ply1degltdimlem  34012  ofcfval4  34495  omsfval  34684  omssubadd  34690  carsgval  34693  sseqval  34778  hgt750lemg  35041  filnetlem4  36892  bj-finsumval0  37929  isrngod  38549  isgrpda  38606  iscringd  38649  sticksstones8  42920  limsupre  46355  limsupval3  46406  limsuppnfdlem  46415  limsupvaluz  46422  limsuppnflem  46424  limsupre2lem  46438  climuzlem  46457  climisp  46460  climxrrelem  46463  climxrre  46464  liminfval5  46479  limsupgtlem  46491  liminfvalxr  46497  liminflelimsupuz  46499  liminfgelimsupuz  46502  liminflimsupclim  46521  liminflbuz2  46529  xlimclim2lem  46553  climxlim2  46560  fourierdlem71  46891  fourierdlem80  46900  sge0val  47080  sge0f1o  47096  isomennd  47245  nsssmfmbflem  47492  isuspgrim  48661  isubgr3stgrlem3  48733  isubgr3stgrlem5  48735  clnbgr3stgrgrlim  48784  itcovalendof  49449  thinccisod  50232