Theorem fexd 7229

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552

This theorem is referenced by:  fidmfisupp  9371  fdmfisuppfi  9372  fsuppco2  9398  fsuppcor  9399  ixpiunwdom  9585  cnfcom3clem  9700  fin23lem32  10339  hasheqf1od  14313  hashf1lem1  14415  hashf1lem1OLD  14416  fz1isolem  14422  ramval  16941  imasval  17457  imasle  17469  pwsco1mhm  18713  efgtf  19590  gsumval3a  19771  gsumval3lem1  19773  gsumval3lem2  19774  gsumval3  19775  gsumzres  19777  gsumzf1o  19780  gsumzaddlem  19789  gsumzadd  19790  gsumzmhm  19805  gsumzoppg  19812  gsumpt  19830  gsum2dlem2  19839  prdslmodd  20580  dsmmsubg  21298  dsmmlss  21299  islindf2  21369  f1lindf  21377  islindf4  21393  gsumply1subr  21756  txcn  23130  prdstps  23133  qtopval2  23200  fmval  23447  tsmsres  23648  tsmsadd  23651  jensen  26493  pwrssmgc  32170  gsumpart  32207  ply1degltdimlem  32707  ofcfval4  33103  omsfval  33293  omssubadd  33299  carsgval  33302  sseqval  33387  hgt750lemg  33666  filnetlem4  35266  bj-finsumval0  36166  isrngod  36766  isgrpda  36823  iscringd  36866  sticksstones8  40969  limsupre  44357  limsupval3  44408  limsuppnfdlem  44417  limsupvaluz  44424  limsuppnflem  44426  limsupre2lem  44440  climuzlem  44459  climisp  44462  climxrrelem  44465  climxrre  44466  liminfval5  44481  limsupgtlem  44493  liminfvalxr  44499  liminflelimsupuz  44501  liminfgelimsupuz  44504  liminflimsupclim  44523  liminflbuz2  44531  xlimclim2lem  44555  climxlim2  44562  fourierdlem71  44893  fourierdlem80  44902  sge0val  45082  sge0f1o  45098  isomennd  45247  nsssmfmbflem  45494  itcovalendof  47355