Theorem fssresd 6690

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

Syntax hints:   → wi 4   ⊆ wss 3902   ↾ cres 5618  ⟶wf 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-fun 6483  df-fn 6484  df-f 6485

This theorem is referenced by:  feqresmpt  6891  resf1extb  7864  resf1ext2b  7865  fsuppcor  9288  ramub2  16926  ramub1lem2  16939  funcres  17803  gsumsplit1r  18595  gasubg  19215  gsumzaddlem  19834  dprdfadd  19935  dprdres  19943  dprdf1  19948  dmdprdsplitlem  19952  dmdprdsplit2lem  19960  dmdprdsplit2  19961  dprdsplit  19963  ablfac1eulem  19987  ablfac1eu  19988  gsumle  20058  pwssplit0  20993  frlmsplit2  21711  mamures  22313  mdetrlin  22518  cnrest  23201  cnpresti  23204  cnprest  23205  ptuncnv  23723  ptunhmeo  23724  ptcmpfi  23729  tsmslem1  24045  tsmssubm  24059  tsmsres  24060  tsmsf1o  24061  tsmsxplem1  24069  tsmsxplem2  24070  psmetres2  24230  xmetres2  24277  metres2  24279  imasdsf1olem  24289  xmetresbl  24353  xrge0gsumle  24750  xrge0tsms  24751  rescncf  24818  mbfres2  25574  limcres  25815  limciun  25823  dvres3  25842  dvmptresicc  25845  dvlip  25926  dvlipcn  25927  dvlip2  25928  dvgt0lem1  25935  dvivthlem1  25941  lhop  25949  ulmres  26325  ulmss  26334  pserdvlem2  26366  jensenlem2  26926  jensen  26927  wlkres  29648  pthdifv  29709  pthdlem1  29745  foresf1o  32482  resf1o  32711  pfxf1  32921  xrge0tsmsd  33040  tocyccntz  33111  elrspunsn  33392  rprmdvdsprod  33497  ply1degltdimlem  33633  zarcmplem  33892  measres  34233  omsmeas  34334  reprsuc  34626  f1resfz0f1d  35156  pfxwlk  35166  pthhashvtx  35170  cvmliftlem6  35332  cvmlift2lem11  35355  satfv1lem  35404  mrsubff1  35556  msubff1  35598  psrbagres  42585  evlselv  42626  fsuppssind  42632  aomclem4  43096  extoimad  44203  imo72b2lem0  44204  imo72b2lem2  44206  imo72b2lem1  44208  imo72b2  44211  wessf1ornlem  45228  feqresmptf  45274  limcperiod  45674  climxlim2  45890  cncfperiod  45923  dirkercncflem4  46150  fourierdlem48  46198  fourierdlem49  46199  fourierdlem51  46201  fourierdlem53  46203  fourierdlem74  46224  fourierdlem75  46225  fourierdlem81  46231  fourierdlem85  46235  fourierdlem88  46238  fourierdlem93  46243  fourierdlem94  46244  fourierdlem95  46245  fourierdlem100  46250  fourierdlem103  46253  fourierdlem104  46254  fourierdlem107  46257  fourierdlem111  46261  fourierdlem112  46262  fourierdlem113  46263  sge0tsms  46424  sge0sup  46435  sge0gerp  46439  sge0pnffigt  46440  sge0lefi  46442  sge0ltfirp  46444  sge0resplit  46450  sge0le  46451  sge0split  46453  sge0iun  46463  meadjun  46506  ismeannd  46511  psmeasurelem  46514  omeunle  46560  omeiunle  46561  caratheodory  46572  hoidmvlelem1  46639  hoidmvlelem2  46640  hoidmvlelem3  46641  hoidmvlelem4  46642  smflimsuplem3  46866  fcoresf1  47106  fcoresfo  47108  lincdifsn  48462