Theorem fssresd 6747

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

Syntax hints:   → wi 4   ⊆ wss 3906   ↾ cres 5665  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  feqresmpt  6952  resf1extb  7932  resf1ext2b  7933  fsuppcor  9365  ramub2  17075  ramub1lem2  17088  funcres  17954  gsumsplit1r  18746  gasubg  19373  gsumzaddlem  19992  dprdfadd  20093  dprdres  20101  dprdf1  20106  dmdprdsplitlem  20110  dmdprdsplit2lem  20118  dmdprdsplit2  20119  dprdsplit  20121  ablfac1eulem  20145  ablfac1eu  20146  gsumle  20216  pwssplit0  21160  frlmsplit2  21904  psrbagres  22061  mamures  22535  mdetrlin  22740  cnrest  23423  cnpresti  23426  cnprest  23427  ptuncnv  23945  ptunhmeo  23946  ptcmpfi  23951  tsmslem1  24267  tsmssubm  24281  tsmsres  24282  tsmsf1o  24283  tsmsxplem1  24291  tsmsxplem2  24292  psmetres2  24452  xmetres2  24499  metres2  24501  imasdsf1olem  24511  xmetresbl  24575  xrge0gsumle  24972  xrge0tsms  24973  rescncf  25037  mbfres2  25785  limcres  26026  limciun  26034  dvres3  26053  dvmptresicc  26056  dvlip  26133  dvlipcn  26134  dvlip2  26135  dvgt0lem1  26142  dvivthlem1  26148  lhop  26156  ulmres  26532  ulmss  26541  pserdvlem2  26572  jensenlem2  27133  jensen  27134  wlkres  29999  pthdifv  30060  pthdlem1  30096  foresf1o  32831  resf1o  33056  pfxf1  33243  xrge0tsmsd  33374  tocyccntz  33445  elrspunsn  33718  rprmdvdsprod  33805  extvfvvcl  33906  extvfvcl  33907  evlextv  33913  esplyind  33946  esplyfvn  33948  vietalem  33950  vieta  33951  ply1degltdimlem  33993  zarcmplem  34252  measres  34593  omsmeas  34694  reprsuc  34983  f1resfz0f1d  35586  pfxwlk  35597  pthhashvtx  35601  cvmliftlem6  35763  cvmlift2lem11  35786  satfv1lem  35835  mrsubff1  35987  msubff1  36029  evlselv  43304  fsuppssind  43308  aomclem4  43767  extoimad  44873  imo72b2lem0  44874  imo72b2lem2  44876  imo72b2lem1  44878  imo72b2  44881  wessf1ornlem  45886  feqresmptf  45929  limcperiod  46327  climxlim2  46543  cncfperiod  46576  dirkercncflem4  46803  fourierdlem48  46851  fourierdlem49  46852  fourierdlem51  46854  fourierdlem53  46856  fourierdlem74  46877  fourierdlem75  46878  fourierdlem81  46884  fourierdlem85  46888  fourierdlem88  46891  fourierdlem93  46896  fourierdlem94  46897  fourierdlem95  46898  fourierdlem100  46903  fourierdlem103  46906  fourierdlem104  46907  fourierdlem107  46910  fourierdlem111  46914  fourierdlem112  46915  fourierdlem113  46916  sge0tsms  47077  sge0sup  47088  sge0gerp  47092  sge0pnffigt  47093  sge0lefi  47095  sge0ltfirp  47097  sge0resplit  47103  sge0le  47104  sge0split  47106  sge0iun  47116  meadjun  47159  ismeannd  47164  psmeasurelem  47167  omeunle  47213  omeiunle  47214  caratheodory  47225  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvlelem4  47295  sssmf  47435  smflimsuplem3  47519  fcoresf1  47789  fcoresfo  47791  lincdifsn  49187