Theorem fexd 7211

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

Syntax hints:   → wi 4   ∈ wcel 2142  Vcvv 3454  ⟶wf 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529

This theorem is referenced by:  mptcnfimad  7967  fidmfisupp  9318  fdmfisuppfi  9320  fsuppco2  9349  fsuppcor  9350  ixpiunwdom  9538  cnfcom3clem  9660  fin23lem32  10301  hasheqf1od  14366  hashf1lem1  14468  fz1isolem  14474  ramval  17044  imasval  17541  imasle  17553  pwsco1mhm  18866  efgtf  19762  gsumval3a  19943  gsumval3lem1  19945  gsumval3lem2  19946  gsumval3  19947  gsumzres  19949  gsumzf1o  19952  gsumzaddlem  19961  gsumzadd  19962  gsumzmhm  19977  gsumzoppg  19984  gsumpt  20002  gsum2dlem2  20011  prdslmodd  21033  dsmmsubg  21792  dsmmlss  21793  islindf2  21863  f1lindf  21871  islindf4  21887  gsumply1subr  22292  txcn  23683  prdstps  23686  qtopval2  23753  fmval  24000  tsmsres  24201  tsmsadd  24204  jensen  27050  fisuppov1  32882  pwrssmgc  33175  gsumpart  33240  gsumwrd2dccat  33255  ply1degltdimlem  33916  ofcfval4  34399  omsfval  34588  omssubadd  34594  carsgval  34597  sseqval  34682  hgt750lemg  34945  filnetlem4  36738  bj-finsumval0  37774  isrngod  38394  isgrpda  38451  iscringd  38494  sticksstones8  42767  limsupre  46212  limsupval3  46263  limsuppnfdlem  46272  limsupvaluz  46279  limsuppnflem  46281  limsupre2lem  46295  climuzlem  46314  climisp  46317  climxrrelem  46320  climxrre  46321  liminfval5  46336  limsupgtlem  46348  liminfvalxr  46354  liminflelimsupuz  46356  liminfgelimsupuz  46359  liminflimsupclim  46378  liminflbuz2  46386  xlimclim2lem  46410  climxlim2  46417  fourierdlem71  46748  fourierdlem80  46757  sge0val  46937  sge0f1o  46953  isomennd  47102  nsssmfmbflem  47349  isuspgrim  48515  isubgr3stgrlem3  48587  isubgr3stgrlem5  48589  clnbgr3stgrgrlim  48638  itcovalendof  49288  thinccisod  50072