Theorem fssresd 6625

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 6624	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ⊆ wss 3883   ↾ cres 5582  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  feqresmpt  6820  fsuppcor  9093  ramub2  16643  ramub1lem2  16656  funcres  17527  gsumsplit1r  18286  gasubg  18823  gsumzaddlem  19437  dprdfadd  19538  dprdres  19546  dprdf1  19551  dmdprdsplitlem  19555  dmdprdsplit2lem  19563  dmdprdsplit2  19564  dprdsplit  19566  ablfac1eulem  19590  ablfac1eu  19591  pwssplit0  20235  frlmsplit2  20890  mamures  21449  mdetrlin  21659  cnrest  22344  cnpresti  22347  cnprest  22348  ptuncnv  22866  ptunhmeo  22867  ptcmpfi  22872  tsmslem1  23188  tsmssubm  23202  tsmsres  23203  tsmsf1o  23204  tsmsxplem1  23212  tsmsxplem2  23213  psmetres2  23375  xmetres2  23422  metres2  23424  imasdsf1olem  23434  xmetresbl  23498  xrge0gsumle  23902  xrge0tsms  23903  rescncf  23966  mbfres2  24714  limcres  24955  limciun  24963  dvres3  24982  dvmptresicc  24985  dvlip  25062  dvlipcn  25063  dvlip2  25064  dvgt0lem1  25071  dvivthlem1  25077  lhop  25085  ulmres  25452  ulmss  25461  pserdvlem2  25492  jensenlem2  26042  jensen  26043  wlkres  27940  pthdlem1  28035  foresf1o  30751  resf1o  30967  pfxf1  31118  xrge0tsmsd  31219  gsumle  31252  tocyccntz  31313  zarcmplem  31733  measres  32090  omsmeas  32190  reprsuc  32495  f1resfz0f1d  32972  pfxwlk  32985  pthhashvtx  32989  cvmliftlem6  33152  cvmlift2lem11  33175  satfv1lem  33224  mrsubff1  33376  msubff1  33418  fsuppssind  40205  aomclem4  40798  extoimad  41664  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2lem1  41669  imo72b2  41672  wessf1ornlem  42611  feqresmptf  42661  limcperiod  43059  climxlim2  43277  cncfperiod  43310  dirkercncflem4  43537  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem53  43590  fourierdlem74  43611  fourierdlem75  43612  fourierdlem81  43618  fourierdlem85  43622  fourierdlem88  43625  fourierdlem93  43630  fourierdlem94  43631  fourierdlem95  43632  fourierdlem100  43637  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  sge0tsms  43808  sge0sup  43819  sge0gerp  43823  sge0pnffigt  43824  sge0lefi  43826  sge0ltfirp  43828  sge0resplit  43834  sge0le  43835  sge0split  43837  sge0iun  43847  meadjun  43890  ismeannd  43895  psmeasurelem  43898  omeunle  43944  omeiunle  43945  caratheodory  43956  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  smflimsuplem3  44242  fcoresf1  44450  fcoresfo  44452  lincdifsn  45653