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

Syntax hints:   → wi 4   ⊆ wss 3890   ↾ cres 5627  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  feqresmpt  6903  resf1extb  7881  resf1ext2b  7882  fsuppcor  9314  ramub2  16983  ramub1lem2  16996  funcres  17861  gsumsplit1r  18653  gasubg  19275  gsumzaddlem  19894  dprdfadd  19995  dprdres  20003  dprdf1  20008  dmdprdsplitlem  20012  dmdprdsplit2lem  20020  dmdprdsplit2  20021  dprdsplit  20023  ablfac1eulem  20047  ablfac1eu  20048  gsumle  20118  pwssplit0  21055  frlmsplit2  21755  psrbagres  21912  mamures  22387  mdetrlin  22592  cnrest  23275  cnpresti  23278  cnprest  23279  ptuncnv  23797  ptunhmeo  23798  ptcmpfi  23803  tsmslem1  24119  tsmssubm  24133  tsmsres  24134  tsmsf1o  24135  tsmsxplem1  24143  tsmsxplem2  24144  psmetres2  24304  xmetres2  24351  metres2  24353  imasdsf1olem  24363  xmetresbl  24427  xrge0gsumle  24824  xrge0tsms  24825  rescncf  24889  mbfres2  25637  limcres  25878  limciun  25886  dvres3  25905  dvmptresicc  25908  dvlip  25985  dvlipcn  25986  dvlip2  25987  dvgt0lem1  25994  dvivthlem1  26000  lhop  26008  ulmres  26378  ulmss  26387  pserdvlem2  26418  jensenlem2  26976  jensen  26977  wlkres  29762  pthdifv  29823  pthdlem1  29859  foresf1o  32599  resf1o  32829  pfxf1  33028  xrge0tsmsd  33161  tocyccntz  33232  elrspunsn  33519  rprmdvdsprod  33624  extvfvvcl  33726  extvfvcl  33727  evlextv  33733  esplyind  33766  esplyfvn  33768  vietalem  33770  vieta  33771  ply1degltdimlem  33813  zarcmplem  34072  measres  34413  omsmeas  34514  reprsuc  34806  f1resfz0f1d  35349  pfxwlk  35359  pthhashvtx  35363  cvmliftlem6  35525  cvmlift2lem11  35548  satfv1lem  35597  mrsubff1  35749  msubff1  35791  evlselv  43046  fsuppssind  43050  aomclem4  43509  extoimad  44615  imo72b2lem0  44616  imo72b2lem2  44618  imo72b2lem1  44620  imo72b2  44623  wessf1ornlem  45639  feqresmptf  45682  limcperiod  46080  climxlim2  46296  cncfperiod  46329  dirkercncflem4  46556  fourierdlem48  46604  fourierdlem49  46605  fourierdlem51  46607  fourierdlem53  46609  fourierdlem74  46630  fourierdlem75  46631  fourierdlem81  46637  fourierdlem85  46641  fourierdlem88  46644  fourierdlem93  46649  fourierdlem94  46650  fourierdlem95  46651  fourierdlem100  46656  fourierdlem103  46659  fourierdlem104  46660  fourierdlem107  46663  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  sge0tsms  46830  sge0sup  46841  sge0gerp  46845  sge0pnffigt  46846  sge0lefi  46848  sge0ltfirp  46850  sge0resplit  46856  sge0le  46857  sge0split  46859  sge0iun  46869  meadjun  46912  ismeannd  46917  psmeasurelem  46920  omeunle  46966  omeiunle  46967  caratheodory  46978  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  smflimsuplem3  47272  fcoresf1  47539  fcoresfo  47541  lincdifsn  48922