Theorem fssresd 6709

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

Syntax hints:   → wi 4   ⊆ wss 3903   ↾ cres 5634  ⟶wf 6496

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  feqresmpt  6911  resf1extb  7886  resf1ext2b  7887  fsuppcor  9319  ramub2  16954  ramub1lem2  16967  funcres  17832  gsumsplit1r  18624  gasubg  19243  gsumzaddlem  19862  dprdfadd  19963  dprdres  19971  dprdf1  19976  dmdprdsplitlem  19980  dmdprdsplit2lem  19988  dmdprdsplit2  19989  dprdsplit  19991  ablfac1eulem  20015  ablfac1eu  20016  gsumle  20086  pwssplit0  21022  frlmsplit2  21740  mamures  22353  mdetrlin  22558  cnrest  23241  cnpresti  23244  cnprest  23245  ptuncnv  23763  ptunhmeo  23764  ptcmpfi  23769  tsmslem1  24085  tsmssubm  24099  tsmsres  24100  tsmsf1o  24101  tsmsxplem1  24109  tsmsxplem2  24110  psmetres2  24270  xmetres2  24317  metres2  24319  imasdsf1olem  24329  xmetresbl  24393  xrge0gsumle  24790  xrge0tsms  24791  rescncf  24858  mbfres2  25614  limcres  25855  limciun  25863  dvres3  25882  dvmptresicc  25885  dvlip  25966  dvlipcn  25967  dvlip2  25968  dvgt0lem1  25975  dvivthlem1  25981  lhop  25989  ulmres  26365  ulmss  26374  pserdvlem2  26406  jensenlem2  26966  jensen  26967  wlkres  29754  pthdifv  29815  pthdlem1  29851  foresf1o  32590  resf1o  32819  pfxf1  33034  xrge0tsmsd  33166  tocyccntz  33237  elrspunsn  33521  rprmdvdsprod  33626  extvfvvcl  33711  extvfvcl  33712  evlextv  33718  esplyind  33751  esplyfvn  33753  vietalem  33755  vieta  33756  ply1degltdimlem  33799  zarcmplem  34058  measres  34399  omsmeas  34500  reprsuc  34792  f1resfz0f1d  35327  pfxwlk  35337  pthhashvtx  35341  cvmliftlem6  35503  cvmlift2lem11  35526  satfv1lem  35575  mrsubff1  35727  msubff1  35769  psrbagres  42911  evlselv  42942  fsuppssind  42948  aomclem4  43411  extoimad  44517  imo72b2lem0  44518  imo72b2lem2  44520  imo72b2lem1  44522  imo72b2  44525  wessf1ornlem  45541  feqresmptf  45586  limcperiod  45985  climxlim2  46201  cncfperiod  46234  dirkercncflem4  46461  fourierdlem48  46509  fourierdlem49  46510  fourierdlem51  46512  fourierdlem53  46514  fourierdlem74  46535  fourierdlem75  46536  fourierdlem81  46542  fourierdlem85  46546  fourierdlem88  46549  fourierdlem93  46554  fourierdlem94  46555  fourierdlem95  46556  fourierdlem100  46561  fourierdlem103  46564  fourierdlem104  46565  fourierdlem107  46568  fourierdlem111  46572  fourierdlem112  46573  fourierdlem113  46574  sge0tsms  46735  sge0sup  46746  sge0gerp  46750  sge0pnffigt  46751  sge0lefi  46753  sge0ltfirp  46755  sge0resplit  46761  sge0le  46762  sge0split  46764  sge0iun  46774  meadjun  46817  ismeannd  46822  psmeasurelem  46825  omeunle  46871  omeiunle  46872  caratheodory  46883  hoidmvlelem1  46950  hoidmvlelem2  46951  hoidmvlelem3  46952  hoidmvlelem4  46953  smflimsuplem3  47177  fcoresf1  47426  fcoresfo  47428  lincdifsn  48781