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 584	1 ⊢ (𝜑 → 𝐹 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474  ⟶wf 6536

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is referenced by:  fidmfisupp  9367  fdmfisuppfi  9368  fsuppco2  9394  fsuppcor  9395  ixpiunwdom  9581  cnfcom3clem  9696  fin23lem32  10335  hasheqf1od  14309  hashf1lem1  14411  hashf1lem1OLD  14412  fz1isolem  14418  ramval  16937  imasval  17453  imasle  17465  pwsco1mhm  18709  efgtf  19584  gsumval3a  19765  gsumval3lem1  19767  gsumval3lem2  19768  gsumval3  19769  gsumzres  19771  gsumzf1o  19774  gsumzaddlem  19783  gsumzadd  19784  gsumzmhm  19799  gsumzoppg  19806  gsumpt  19824  gsum2dlem2  19833  prdslmodd  20572  dsmmsubg  21289  dsmmlss  21290  islindf2  21360  f1lindf  21368  islindf4  21384  gsumply1subr  21747  txcn  23121  prdstps  23124  qtopval2  23191  fmval  23438  tsmsres  23639  tsmsadd  23642  jensen  26482  pwrssmgc  32157  gsumpart  32194  ply1degltdimlem  32695  ofcfval4  33091  omsfval  33281  omssubadd  33287  carsgval  33290  sseqval  33375  hgt750lemg  33654  filnetlem4  35254  bj-finsumval0  36154  isrngod  36754  isgrpda  36811  iscringd  36854  sticksstones8  40957  limsupre  44343  limsupval3  44394  limsuppnfdlem  44403  limsupvaluz  44410  limsuppnflem  44412  limsupre2lem  44426  climuzlem  44445  climisp  44448  climxrrelem  44451  climxrre  44452  liminfval5  44467  limsupgtlem  44479  liminfvalxr  44485  liminflelimsupuz  44487  liminfgelimsupuz  44490  liminflimsupclim  44509  liminflbuz2  44517  xlimclim2lem  44541  climxlim2  44548  fourierdlem71  44879  fourierdlem80  44888  sge0val  45068  sge0f1o  45084  isomennd  45233  nsssmfmbflem  45480  itcovalendof  47308