Theorem fexd 7247

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  ⟶wf 6557

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569

This theorem is referenced by:  mptcnfimad  8011  fidmfisupp  9412  fdmfisuppfi  9414  fsuppco2  9443  fsuppcor  9444  ixpiunwdom  9630  cnfcom3clem  9745  fin23lem32  10384  hasheqf1od  14392  hashf1lem1  14494  fz1isolem  14500  ramval  17046  imasval  17556  imasle  17568  pwsco1mhm  18845  efgtf  19740  gsumval3a  19921  gsumval3lem1  19923  gsumval3lem2  19924  gsumval3  19925  gsumzres  19927  gsumzf1o  19930  gsumzaddlem  19939  gsumzadd  19940  gsumzmhm  19955  gsumzoppg  19962  gsumpt  19980  gsum2dlem2  19989  prdslmodd  20967  dsmmsubg  21763  dsmmlss  21764  islindf2  21834  f1lindf  21842  islindf4  21858  gsumply1subr  22235  txcn  23634  prdstps  23637  qtopval2  23704  fmval  23951  tsmsres  24152  tsmsadd  24155  jensen  27032  fisuppov1  32692  pwrssmgc  32990  gsumpart  33060  gsumwrd2dccat  33070  ply1degltdimlem  33673  ofcfval4  34106  omsfval  34296  omssubadd  34302  carsgval  34305  sseqval  34390  hgt750lemg  34669  filnetlem4  36382  bj-finsumval0  37286  isrngod  37905  isgrpda  37962  iscringd  38005  sticksstones8  42154  limsupre  45656  limsupval3  45707  limsuppnfdlem  45716  limsupvaluz  45723  limsuppnflem  45725  limsupre2lem  45739  climuzlem  45758  climisp  45761  climxrrelem  45764  climxrre  45765  liminfval5  45780  limsupgtlem  45792  liminfvalxr  45798  liminflelimsupuz  45800  liminfgelimsupuz  45803  liminflimsupclim  45822  liminflbuz2  45830  xlimclim2lem  45854  climxlim2  45861  fourierdlem71  46192  fourierdlem80  46201  sge0val  46381  sge0f1o  46397  isomennd  46546  nsssmfmbflem  46793  isuspgrim  47875  isubgr3stgrlem3  47935  isubgr3stgrlem5  47937  itcovalendof  48590  thinccisod  49103