Theorem fexd 7226

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463  ⟶wf 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is referenced by:  mptcnfimad  7982  fidmfisupp  9331  fdmfisuppfi  9333  fsuppco2  9362  fsuppcor  9363  ixpiunwdom  9551  cnfcom3clem  9673  fin23lem32  10327  hasheqf1od  14388  hashf1lem1  14491  fz1isolem  14497  ramval  17067  imasval  17564  imasle  17576  pwsco1mhm  18890  efgtf  19791  gsumval3a  19972  gsumval3lem1  19974  gsumval3lem2  19975  gsumval3  19976  gsumzres  19978  gsumzf1o  19981  gsumzaddlem  19990  gsumzadd  19991  gsumzmhm  20006  gsumzoppg  20013  gsumpt  20031  gsum2dlem2  20040  prdslmodd  21067  dsmmsubg  21861  dsmmlss  21862  islindf2  21932  f1lindf  21940  islindf4  21956  gsumply1subr  22361  txcn  23751  prdstps  23754  qtopval2  23821  fmval  24068  tsmsres  24269  tsmsadd  24272  jensen  27118  fisuppov1  32968  pwrssmgc  33260  gsumpart  33323  gsumwrd2dccat  33338  ply1degltdimlem  33956  ofcfval4  34439  omsfval  34628  omssubadd  34634  carsgval  34637  sseqval  34722  hgt750lemg  34985  filnetlem4  36780  bj-finsumval0  37816  isrngod  38436  isgrpda  38493  iscringd  38536  sticksstones8  42809  limsupre  46246  limsupval3  46297  limsuppnfdlem  46306  limsupvaluz  46313  limsuppnflem  46315  limsupre2lem  46329  climuzlem  46348  climisp  46351  climxrrelem  46354  climxrre  46355  liminfval5  46370  limsupgtlem  46382  liminfvalxr  46388  liminflelimsupuz  46390  liminfgelimsupuz  46393  liminflimsupclim  46412  liminflbuz2  46420  xlimclim2lem  46444  climxlim2  46451  fourierdlem71  46782  fourierdlem80  46791  sge0val  46971  sge0f1o  46987  isomennd  47136  nsssmfmbflem  47383  isuspgrim  48549  isubgr3stgrlem3  48621  isubgr3stgrlem5  48623  clnbgr3stgrgrlim  48672  itcovalendof  49333  thinccisod  50116