Theorem fssresd 6758

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

Syntax hints:   → wi 4   ⊆ wss 3948   ↾ cres 5678  ⟶wf 6539

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  feqresmpt  6961  fsuppcor  9401  ramub2  16951  ramub1lem2  16964  funcres  17850  gsumsplit1r  18612  gasubg  19207  gsumzaddlem  19830  dprdfadd  19931  dprdres  19939  dprdf1  19944  dmdprdsplitlem  19948  dmdprdsplit2lem  19956  dmdprdsplit2  19957  dprdsplit  19959  ablfac1eulem  19983  ablfac1eu  19984  pwssplit0  20813  frlmsplit2  21547  mamures  22112  mdetrlin  22324  cnrest  23009  cnpresti  23012  cnprest  23013  ptuncnv  23531  ptunhmeo  23532  ptcmpfi  23537  tsmslem1  23853  tsmssubm  23867  tsmsres  23868  tsmsf1o  23869  tsmsxplem1  23877  tsmsxplem2  23878  psmetres2  24040  xmetres2  24087  metres2  24089  imasdsf1olem  24099  xmetresbl  24163  xrge0gsumle  24569  xrge0tsms  24570  rescncf  24637  mbfres2  25386  limcres  25627  limciun  25635  dvres3  25654  dvmptresicc  25657  dvlip  25734  dvlipcn  25735  dvlip2  25736  dvgt0lem1  25743  dvivthlem1  25749  lhop  25757  ulmres  26124  ulmss  26133  pserdvlem2  26164  jensenlem2  26716  jensen  26717  wlkres  29182  pthdlem1  29278  foresf1o  31997  resf1o  32210  pfxf1  32363  xrge0tsmsd  32467  gsumle  32500  tocyccntz  32561  elrspunsn  32809  ply1degltdimlem  32983  zarcmplem  33147  measres  33506  omsmeas  33608  reprsuc  33913  f1resfz0f1d  34389  pfxwlk  34400  pthhashvtx  34404  cvmliftlem6  34567  cvmlift2lem11  34590  satfv1lem  34639  mrsubff1  34791  msubff1  34833  psrbagres  41417  evlselv  41461  fsuppssind  41467  aomclem4  42101  extoimad  43218  imo72b2lem0  43219  imo72b2lem2  43221  imo72b2lem1  43223  imo72b2  43226  wessf1ornlem  44183  feqresmptf  44230  limcperiod  44643  climxlim2  44861  cncfperiod  44894  dirkercncflem4  45121  fourierdlem48  45169  fourierdlem49  45170  fourierdlem51  45172  fourierdlem53  45174  fourierdlem74  45195  fourierdlem75  45196  fourierdlem81  45202  fourierdlem85  45206  fourierdlem88  45209  fourierdlem93  45214  fourierdlem94  45215  fourierdlem95  45216  fourierdlem100  45221  fourierdlem103  45224  fourierdlem104  45225  fourierdlem107  45228  fourierdlem111  45232  fourierdlem112  45233  fourierdlem113  45234  sge0tsms  45395  sge0sup  45406  sge0gerp  45410  sge0pnffigt  45411  sge0lefi  45413  sge0ltfirp  45415  sge0resplit  45421  sge0le  45422  sge0split  45424  sge0iun  45434  meadjun  45477  ismeannd  45482  psmeasurelem  45485  omeunle  45531  omeiunle  45532  caratheodory  45543  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  smflimsuplem3  45837  fcoresf1  46078  fcoresfo  46080  lincdifsn  47193