Theorem fexd 7183

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508

This theorem is referenced by:  mptcnfimad  7940  fidmfisupp  9287  fdmfisuppfi  9289  fsuppco2  9318  fsuppcor  9319  ixpiunwdom  9507  cnfcom3clem  9626  fin23lem32  10266  hasheqf1od  14288  hashf1lem1  14390  fz1isolem  14396  ramval  16948  imasval  17444  imasle  17456  pwsco1mhm  18769  efgtf  19663  gsumval3a  19844  gsumval3lem1  19846  gsumval3lem2  19847  gsumval3  19848  gsumzres  19850  gsumzf1o  19853  gsumzaddlem  19862  gsumzadd  19863  gsumzmhm  19878  gsumzoppg  19885  gsumpt  19903  gsum2dlem2  19912  prdslmodd  20932  dsmmsubg  21710  dsmmlss  21711  islindf2  21781  f1lindf  21789  islindf4  21805  gsumply1subr  22186  txcn  23582  prdstps  23585  qtopval2  23652  fmval  23899  tsmsres  24100  tsmsadd  24103  jensen  26967  fisuppov1  32773  pwrssmgc  33093  gsumpart  33157  gsumwrd2dccat  33172  ply1degltdimlem  33800  ofcfval4  34283  omsfval  34472  omssubadd  34478  carsgval  34481  sseqval  34566  hgt750lemg  34832  filnetlem4  36597  bj-finsumval0  37540  isrngod  38149  isgrpda  38206  iscringd  38249  sticksstones8  42523  limsupre  45999  limsupval3  46050  limsuppnfdlem  46059  limsupvaluz  46066  limsuppnflem  46068  limsupre2lem  46082  climuzlem  46101  climisp  46104  climxrrelem  46107  climxrre  46108  liminfval5  46123  limsupgtlem  46135  liminfvalxr  46141  liminflelimsupuz  46143  liminfgelimsupuz  46146  liminflimsupclim  46165  liminflbuz2  46173  xlimclim2lem  46197  climxlim2  46204  fourierdlem71  46535  fourierdlem80  46544  sge0val  46724  sge0f1o  46740  isomennd  46889  nsssmfmbflem  47136  isuspgrim  48256  isubgr3stgrlem3  48328  isubgr3stgrlem5  48330  clnbgr3stgrgrlim  48379  itcovalendof  49029  thinccisod  49813