Theorem fssresd 6641

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

Syntax hints:   → wi 4   ⊆ wss 3887   ↾ cres 5591  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-fun 6435  df-fn 6436  df-f 6437

This theorem is referenced by:  feqresmpt  6838  fsuppcor  9163  ramub2  16715  ramub1lem2  16728  funcres  17611  gsumsplit1r  18371  gasubg  18908  gsumzaddlem  19522  dprdfadd  19623  dprdres  19631  dprdf1  19636  dmdprdsplitlem  19640  dmdprdsplit2lem  19648  dmdprdsplit2  19649  dprdsplit  19651  ablfac1eulem  19675  ablfac1eu  19676  pwssplit0  20320  frlmsplit2  20980  mamures  21539  mdetrlin  21751  cnrest  22436  cnpresti  22439  cnprest  22440  ptuncnv  22958  ptunhmeo  22959  ptcmpfi  22964  tsmslem1  23280  tsmssubm  23294  tsmsres  23295  tsmsf1o  23296  tsmsxplem1  23304  tsmsxplem2  23305  psmetres2  23467  xmetres2  23514  metres2  23516  imasdsf1olem  23526  xmetresbl  23590  xrge0gsumle  23996  xrge0tsms  23997  rescncf  24060  mbfres2  24809  limcres  25050  limciun  25058  dvres3  25077  dvmptresicc  25080  dvlip  25157  dvlipcn  25158  dvlip2  25159  dvgt0lem1  25166  dvivthlem1  25172  lhop  25180  ulmres  25547  ulmss  25556  pserdvlem2  25587  jensenlem2  26137  jensen  26138  wlkres  28038  pthdlem1  28134  foresf1o  30850  resf1o  31065  pfxf1  31216  xrge0tsmsd  31317  gsumle  31350  tocyccntz  31411  zarcmplem  31831  measres  32190  omsmeas  32290  reprsuc  32595  f1resfz0f1d  33072  pfxwlk  33085  pthhashvtx  33089  cvmliftlem6  33252  cvmlift2lem11  33275  satfv1lem  33324  mrsubff1  33476  msubff1  33518  fsuppssind  40282  aomclem4  40882  extoimad  41775  imo72b2lem0  41776  imo72b2lem2  41778  imo72b2lem1  41780  imo72b2  41783  wessf1ornlem  42722  feqresmptf  42772  limcperiod  43169  climxlim2  43387  cncfperiod  43420  dirkercncflem4  43647  fourierdlem48  43695  fourierdlem49  43696  fourierdlem51  43698  fourierdlem53  43700  fourierdlem74  43721  fourierdlem75  43722  fourierdlem81  43728  fourierdlem85  43732  fourierdlem88  43735  fourierdlem93  43740  fourierdlem94  43741  fourierdlem95  43742  fourierdlem100  43747  fourierdlem103  43750  fourierdlem104  43751  fourierdlem107  43754  fourierdlem111  43758  fourierdlem112  43759  fourierdlem113  43760  sge0tsms  43918  sge0sup  43929  sge0gerp  43933  sge0pnffigt  43934  sge0lefi  43936  sge0ltfirp  43938  sge0resplit  43944  sge0le  43945  sge0split  43947  sge0iun  43957  meadjun  44000  ismeannd  44005  psmeasurelem  44008  omeunle  44054  omeiunle  44055  caratheodory  44066  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvlelem4  44136  smflimsuplem3  44355  fcoresf1  44563  fcoresfo  44565  lincdifsn  45765