Theorem fssresd 6701

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

Syntax hints:   → wi 4   ⊆ wss 3890   ↾ cres 5626  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  feqresmpt  6903  resf1extb  7878  resf1ext2b  7879  fsuppcor  9310  ramub2  16976  ramub1lem2  16989  funcres  17854  gsumsplit1r  18646  gasubg  19268  gsumzaddlem  19887  dprdfadd  19988  dprdres  19996  dprdf1  20001  dmdprdsplitlem  20005  dmdprdsplit2lem  20013  dmdprdsplit2  20014  dprdsplit  20016  ablfac1eulem  20040  ablfac1eu  20041  gsumle  20111  pwssplit0  21045  frlmsplit2  21763  mamures  22372  mdetrlin  22577  cnrest  23260  cnpresti  23263  cnprest  23264  ptuncnv  23782  ptunhmeo  23783  ptcmpfi  23788  tsmslem1  24104  tsmssubm  24118  tsmsres  24119  tsmsf1o  24120  tsmsxplem1  24128  tsmsxplem2  24129  psmetres2  24289  xmetres2  24336  metres2  24338  imasdsf1olem  24348  xmetresbl  24412  xrge0gsumle  24809  xrge0tsms  24810  rescncf  24874  mbfres2  25622  limcres  25863  limciun  25871  dvres3  25890  dvmptresicc  25893  dvlip  25970  dvlipcn  25971  dvlip2  25972  dvgt0lem1  25979  dvivthlem1  25985  lhop  25993  ulmres  26366  ulmss  26375  pserdvlem2  26406  jensenlem2  26965  jensen  26966  wlkres  29752  pthdifv  29813  pthdlem1  29849  foresf1o  32589  resf1o  32818  pfxf1  33017  xrge0tsmsd  33149  tocyccntz  33220  elrspunsn  33504  rprmdvdsprod  33609  extvfvvcl  33694  extvfvcl  33695  evlextv  33701  esplyind  33734  esplyfvn  33736  vietalem  33738  vieta  33739  ply1degltdimlem  33782  zarcmplem  34041  measres  34382  omsmeas  34483  reprsuc  34775  f1resfz0f1d  35312  pfxwlk  35322  pthhashvtx  35326  cvmliftlem6  35488  cvmlift2lem11  35511  satfv1lem  35560  mrsubff1  35712  msubff1  35754  psrbagres  43003  evlselv  43034  fsuppssind  43040  aomclem4  43503  extoimad  44609  imo72b2lem0  44610  imo72b2lem2  44612  imo72b2lem1  44614  imo72b2  44617  wessf1ornlem  45633  feqresmptf  45678  limcperiod  46076  climxlim2  46292  cncfperiod  46325  dirkercncflem4  46552  fourierdlem48  46600  fourierdlem49  46601  fourierdlem51  46603  fourierdlem53  46605  fourierdlem74  46626  fourierdlem75  46627  fourierdlem81  46633  fourierdlem85  46637  fourierdlem88  46640  fourierdlem93  46645  fourierdlem94  46646  fourierdlem95  46647  fourierdlem100  46652  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  sge0tsms  46826  sge0sup  46837  sge0gerp  46841  sge0pnffigt  46842  sge0lefi  46844  sge0ltfirp  46846  sge0resplit  46852  sge0le  46853  sge0split  46855  sge0iun  46865  meadjun  46908  ismeannd  46913  psmeasurelem  46916  omeunle  46962  omeiunle  46963  caratheodory  46974  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  smflimsuplem3  47268  fcoresf1  47529  fcoresfo  47531  lincdifsn  48912