Theorem fssresd 6686

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

Syntax hints:   → wi 4   ⊆ wss 3897   ↾ cres 5616  ⟶wf 6469

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-br 5090  df-opab 5152  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-fun 6475  df-fn 6476  df-f 6477

This theorem is referenced by:  feqresmpt  6888  fsuppcor  9253  ramub2  16804  ramub1lem2  16817  funcres  17700  gsumsplit1r  18460  gasubg  18996  gsumzaddlem  19609  dprdfadd  19710  dprdres  19718  dprdf1  19723  dmdprdsplitlem  19727  dmdprdsplit2lem  19735  dmdprdsplit2  19736  dprdsplit  19738  ablfac1eulem  19762  ablfac1eu  19763  pwssplit0  20418  frlmsplit2  21078  mamures  21637  mdetrlin  21849  cnrest  22534  cnpresti  22537  cnprest  22538  ptuncnv  23056  ptunhmeo  23057  ptcmpfi  23062  tsmslem1  23378  tsmssubm  23392  tsmsres  23393  tsmsf1o  23394  tsmsxplem1  23402  tsmsxplem2  23403  psmetres2  23565  xmetres2  23612  metres2  23614  imasdsf1olem  23624  xmetresbl  23688  xrge0gsumle  24094  xrge0tsms  24095  rescncf  24158  mbfres2  24907  limcres  25148  limciun  25156  dvres3  25175  dvmptresicc  25178  dvlip  25255  dvlipcn  25256  dvlip2  25257  dvgt0lem1  25264  dvivthlem1  25270  lhop  25278  ulmres  25645  ulmss  25654  pserdvlem2  25685  jensenlem2  26235  jensen  26236  wlkres  28267  pthdlem1  28363  foresf1o  31079  resf1o  31293  pfxf1  31444  xrge0tsmsd  31545  gsumle  31578  tocyccntz  31639  zarcmplem  32070  measres  32429  omsmeas  32531  reprsuc  32836  f1resfz0f1d  33312  pfxwlk  33325  pthhashvtx  33329  cvmliftlem6  33492  cvmlift2lem11  33515  satfv1lem  33564  mrsubff1  33716  msubff1  33758  fsuppssind  40532  aomclem4  41133  extoimad  42085  imo72b2lem0  42086  imo72b2lem2  42088  imo72b2lem1  42090  imo72b2  42093  wessf1ornlem  43038  feqresmptf  43089  limcperiod  43494  climxlim2  43712  cncfperiod  43745  dirkercncflem4  43972  fourierdlem48  44020  fourierdlem49  44021  fourierdlem51  44023  fourierdlem53  44025  fourierdlem74  44046  fourierdlem75  44047  fourierdlem81  44053  fourierdlem85  44057  fourierdlem88  44060  fourierdlem93  44065  fourierdlem94  44066  fourierdlem95  44067  fourierdlem100  44072  fourierdlem103  44075  fourierdlem104  44076  fourierdlem107  44079  fourierdlem111  44083  fourierdlem112  44084  fourierdlem113  44085  sge0tsms  44244  sge0sup  44255  sge0gerp  44259  sge0pnffigt  44260  sge0lefi  44262  sge0ltfirp  44264  sge0resplit  44270  sge0le  44271  sge0split  44273  sge0iun  44283  meadjun  44326  ismeannd  44331  psmeasurelem  44334  omeunle  44380  omeiunle  44381  caratheodory  44392  hoidmvlelem1  44459  hoidmvlelem2  44460  hoidmvlelem3  44461  hoidmvlelem4  44462  smflimsuplem3  44686  fcoresf1  44903  fcoresfo  44905  lincdifsn  46105