Theorem fssresd 6725

Description: Restriction of a function with a subclass of its domain, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fssresd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fssresd.2	⊢ (𝜑 → 𝐶 ⊆ 𝐴)

Assertion

Ref	Expression
fssresd	⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Proof of Theorem fssresd

Step	Hyp	Ref	Expression
1		fssresd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fssresd.2	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
3		fssres 6724	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ⊆ wss 3902   ↾ cres 5645  ⟶wf 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-fun 6517  df-fn 6518  df-f 6519

This theorem is referenced by:  feqresmpt  6930  resf1extb  7909  resf1ext2b  7910  fsuppcor  9343  ramub2  17040  ramub1lem2  17053  funcres  17919  gsumsplit1r  18711  gasubg  19332  gsumzaddlem  19951  dprdfadd  20052  dprdres  20060  dprdf1  20065  dmdprdsplitlem  20069  dmdprdsplit2lem  20077  dmdprdsplit2  20078  dprdsplit  20080  ablfac1eulem  20104  ablfac1eu  20105  gsumle  20175  pwssplit0  21112  frlmsplit2  21812  psrbagres  21969  mamures  22444  mdetrlin  22649  cnrest  23332  cnpresti  23335  cnprest  23336  ptuncnv  23854  ptunhmeo  23855  ptcmpfi  23860  tsmslem1  24176  tsmssubm  24190  tsmsres  24191  tsmsf1o  24192  tsmsxplem1  24200  tsmsxplem2  24201  psmetres2  24361  xmetres2  24408  metres2  24410  imasdsf1olem  24420  xmetresbl  24484  xrge0gsumle  24881  xrge0tsms  24882  rescncf  24946  mbfres2  25694  limcres  25935  limciun  25943  dvres3  25962  dvmptresicc  25965  dvlip  26042  dvlipcn  26043  dvlip2  26044  dvgt0lem1  26051  dvivthlem1  26057  lhop  26065  ulmres  26438  ulmss  26447  pserdvlem2  26478  jensenlem2  27039  jensen  27040  wlkres  29825  pthdifv  29886  pthdlem1  29922  foresf1o  32662  resf1o  32892  pfxf1  33080  xrge0tsmsd  33213  tocyccntz  33284  elrspunsn  33575  rprmdvdsprod  33690  extvfvvcl  33792  extvfvcl  33793  evlextv  33799  esplyind  33832  esplyfvn  33834  vietalem  33836  vieta  33837  ply1degltdimlem  33879  zarcmplem  34138  measres  34479  omsmeas  34580  reprsuc  34869  f1resfz0f1d  35424  pfxwlk  35434  pthhashvtx  35438  cvmliftlem6  35600  cvmlift2lem11  35623  satfv1lem  35672  mrsubff1  35824  msubff1  35866  evlselv  43131  fsuppssind  43135  aomclem4  43594  extoimad  44700  imo72b2lem0  44701  imo72b2lem2  44703  imo72b2lem1  44705  imo72b2  44708  wessf1ornlem  45723  feqresmptf  45766  limcperiod  46164  climxlim2  46380  cncfperiod  46413  dirkercncflem4  46640  fourierdlem48  46688  fourierdlem49  46689  fourierdlem51  46691  fourierdlem53  46693  fourierdlem74  46714  fourierdlem75  46715  fourierdlem81  46721  fourierdlem85  46725  fourierdlem88  46728  fourierdlem93  46733  fourierdlem94  46734  fourierdlem95  46735  fourierdlem100  46740  fourierdlem103  46743  fourierdlem104  46744  fourierdlem107  46747  fourierdlem111  46751  fourierdlem112  46752  fourierdlem113  46753  sge0tsms  46914  sge0sup  46925  sge0gerp  46929  sge0pnffigt  46930  sge0lefi  46932  sge0ltfirp  46934  sge0resplit  46940  sge0le  46941  sge0split  46943  sge0iun  46953  meadjun  46996  ismeannd  47001  psmeasurelem  47004  omeunle  47050  omeiunle  47051  caratheodory  47062  hoidmvlelem1  47129  hoidmvlelem2  47130  hoidmvlelem3  47131  hoidmvlelem4  47132  sssmf  47272  smflimsuplem3  47356  fcoresf1  47623  fcoresfo  47625  lincdifsn  49006