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 584	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

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

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  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  7876  resf1ext2b  7877  fsuppcor  9307  ramub2  16942  ramub1lem2  16955  funcres  17820  gsumsplit1r  18612  gasubg  19231  gsumzaddlem  19850  dprdfadd  19951  dprdres  19959  dprdf1  19964  dmdprdsplitlem  19968  dmdprdsplit2lem  19976  dmdprdsplit2  19977  dprdsplit  19979  ablfac1eulem  20003  ablfac1eu  20004  gsumle  20074  pwssplit0  21010  frlmsplit2  21728  mamures  22341  mdetrlin  22546  cnrest  23229  cnpresti  23232  cnprest  23233  ptuncnv  23751  ptunhmeo  23752  ptcmpfi  23757  tsmslem1  24073  tsmssubm  24087  tsmsres  24088  tsmsf1o  24089  tsmsxplem1  24097  tsmsxplem2  24098  psmetres2  24258  xmetres2  24305  metres2  24307  imasdsf1olem  24317  xmetresbl  24381  xrge0gsumle  24778  xrge0tsms  24779  rescncf  24846  mbfres2  25602  limcres  25843  limciun  25851  dvres3  25870  dvmptresicc  25873  dvlip  25954  dvlipcn  25955  dvlip2  25956  dvgt0lem1  25963  dvivthlem1  25969  lhop  25977  ulmres  26353  ulmss  26362  pserdvlem2  26394  jensenlem2  26954  jensen  26955  wlkres  29742  pthdifv  29803  pthdlem1  29839  foresf1o  32579  resf1o  32809  pfxf1  33024  xrge0tsmsd  33155  tocyccntz  33226  elrspunsn  33510  rprmdvdsprod  33615  extvfvvcl  33700  extvfvcl  33701  evlextv  33707  esplyind  33731  esplyfvn  33733  vietalem  33735  vieta  33736  ply1degltdimlem  33779  zarcmplem  34038  measres  34379  omsmeas  34480  reprsuc  34772  f1resfz0f1d  35308  pfxwlk  35318  pthhashvtx  35322  cvmliftlem6  35484  cvmlift2lem11  35507  satfv1lem  35556  mrsubff1  35708  msubff1  35750  psrbagres  42799  evlselv  42830  fsuppssind  42836  aomclem4  43299  extoimad  44405  imo72b2lem0  44406  imo72b2lem2  44408  imo72b2lem1  44410  imo72b2  44413  wessf1ornlem  45429  feqresmptf  45475  limcperiod  45874  climxlim2  46090  cncfperiod  46123  dirkercncflem4  46350  fourierdlem48  46398  fourierdlem49  46399  fourierdlem51  46401  fourierdlem53  46403  fourierdlem74  46424  fourierdlem75  46425  fourierdlem81  46431  fourierdlem85  46435  fourierdlem88  46438  fourierdlem93  46443  fourierdlem94  46444  fourierdlem95  46445  fourierdlem100  46450  fourierdlem103  46453  fourierdlem104  46454  fourierdlem107  46457  fourierdlem111  46461  fourierdlem112  46462  fourierdlem113  46463  sge0tsms  46624  sge0sup  46635  sge0gerp  46639  sge0pnffigt  46640  sge0lefi  46642  sge0ltfirp  46644  sge0resplit  46650  sge0le  46651  sge0split  46653  sge0iun  46663  meadjun  46706  ismeannd  46711  psmeasurelem  46714  omeunle  46760  omeiunle  46761  caratheodory  46772  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  smflimsuplem3  47066  fcoresf1  47315  fcoresfo  47317  lincdifsn  48670