Theorem fssresd 6707

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

Syntax hints:   → wi 4   ⊆ wss 3889   ↾ cres 5633  ⟶wf 6494

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  feqresmpt  6909  resf1extb  7885  resf1ext2b  7886  fsuppcor  9317  ramub2  16985  ramub1lem2  16998  funcres  17863  gsumsplit1r  18655  gasubg  19277  gsumzaddlem  19896  dprdfadd  19997  dprdres  20005  dprdf1  20010  dmdprdsplitlem  20014  dmdprdsplit2lem  20022  dmdprdsplit2  20023  dprdsplit  20025  ablfac1eulem  20049  ablfac1eu  20050  gsumle  20120  pwssplit0  21053  frlmsplit2  21753  mamures  22362  mdetrlin  22567  cnrest  23250  cnpresti  23253  cnprest  23254  ptuncnv  23772  ptunhmeo  23773  ptcmpfi  23778  tsmslem1  24094  tsmssubm  24108  tsmsres  24109  tsmsf1o  24110  tsmsxplem1  24118  tsmsxplem2  24119  psmetres2  24279  xmetres2  24326  metres2  24328  imasdsf1olem  24338  xmetresbl  24402  xrge0gsumle  24799  xrge0tsms  24800  rescncf  24864  mbfres2  25612  limcres  25853  limciun  25861  dvres3  25880  dvmptresicc  25883  dvlip  25960  dvlipcn  25961  dvlip2  25962  dvgt0lem1  25969  dvivthlem1  25975  lhop  25983  ulmres  26353  ulmss  26362  pserdvlem2  26393  jensenlem2  26951  jensen  26952  wlkres  29737  pthdifv  29798  pthdlem1  29834  foresf1o  32574  resf1o  32803  pfxf1  33002  xrge0tsmsd  33134  tocyccntz  33205  elrspunsn  33489  rprmdvdsprod  33594  extvfvvcl  33679  extvfvcl  33680  evlextv  33686  esplyind  33719  esplyfvn  33721  vietalem  33723  vieta  33724  ply1degltdimlem  33766  zarcmplem  34025  measres  34366  omsmeas  34467  reprsuc  34759  f1resfz0f1d  35296  pfxwlk  35306  pthhashvtx  35310  cvmliftlem6  35472  cvmlift2lem11  35495  satfv1lem  35544  mrsubff1  35696  msubff1  35738  psrbagres  42989  evlselv  43020  fsuppssind  43026  aomclem4  43485  extoimad  44591  imo72b2lem0  44592  imo72b2lem2  44594  imo72b2lem1  44596  imo72b2  44599  wessf1ornlem  45615  feqresmptf  45660  limcperiod  46058  climxlim2  46274  cncfperiod  46307  dirkercncflem4  46534  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem53  46587  fourierdlem74  46608  fourierdlem75  46609  fourierdlem81  46615  fourierdlem85  46619  fourierdlem88  46622  fourierdlem93  46627  fourierdlem94  46628  fourierdlem95  46629  fourierdlem100  46634  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  sge0tsms  46808  sge0sup  46819  sge0gerp  46823  sge0pnffigt  46824  sge0lefi  46826  sge0ltfirp  46828  sge0resplit  46834  sge0le  46835  sge0split  46837  sge0iun  46847  meadjun  46890  ismeannd  46895  psmeasurelem  46898  omeunle  46944  omeiunle  46945  caratheodory  46956  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  smflimsuplem3  47250  fcoresf1  47517  fcoresfo  47519  lincdifsn  48900