Theorem fexd 7204

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522

This theorem is referenced by:  mptcnfimad  7968  fidmfisupp  9330  fdmfisuppfi  9332  fsuppco2  9361  fsuppcor  9362  ixpiunwdom  9550  cnfcom3clem  9665  fin23lem32  10304  hasheqf1od  14325  hashf1lem1  14427  fz1isolem  14433  ramval  16986  imasval  17481  imasle  17493  pwsco1mhm  18766  efgtf  19659  gsumval3a  19840  gsumval3lem1  19842  gsumval3lem2  19843  gsumval3  19844  gsumzres  19846  gsumzf1o  19849  gsumzaddlem  19858  gsumzadd  19859  gsumzmhm  19874  gsumzoppg  19881  gsumpt  19899  gsum2dlem2  19908  prdslmodd  20882  dsmmsubg  21659  dsmmlss  21660  islindf2  21730  f1lindf  21738  islindf4  21754  gsumply1subr  22125  txcn  23520  prdstps  23523  qtopval2  23590  fmval  23837  tsmsres  24038  tsmsadd  24041  jensen  26906  fisuppov1  32613  pwrssmgc  32933  gsumpart  33004  gsumwrd2dccat  33014  ply1degltdimlem  33625  ofcfval4  34102  omsfval  34292  omssubadd  34298  carsgval  34301  sseqval  34386  hgt750lemg  34652  filnetlem4  36376  bj-finsumval0  37280  isrngod  37899  isgrpda  37956  iscringd  37999  sticksstones8  42148  limsupre  45646  limsupval3  45697  limsuppnfdlem  45706  limsupvaluz  45713  limsuppnflem  45715  limsupre2lem  45729  climuzlem  45748  climisp  45751  climxrrelem  45754  climxrre  45755  liminfval5  45770  limsupgtlem  45782  liminfvalxr  45788  liminflelimsupuz  45790  liminfgelimsupuz  45793  liminflimsupclim  45812  liminflbuz2  45820  xlimclim2lem  45844  climxlim2  45851  fourierdlem71  46182  fourierdlem80  46191  sge0val  46371  sge0f1o  46387  isomennd  46536  nsssmfmbflem  46783  isuspgrim  47900  isubgr3stgrlem3  47971  isubgr3stgrlem5  47973  itcovalendof  48662  thinccisod  49447