Theorem fssresd 6695

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

Syntax hints:   → wi 4   ⊆ wss 3905   ↾ cres 5625  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  feqresmpt  6896  resf1extb  7874  resf1ext2b  7875  fsuppcor  9313  ramub2  16944  ramub1lem2  16957  funcres  17821  gsumsplit1r  18579  gasubg  19199  gsumzaddlem  19818  dprdfadd  19919  dprdres  19927  dprdf1  19932  dmdprdsplitlem  19936  dmdprdsplit2lem  19944  dmdprdsplit2  19945  dprdsplit  19947  ablfac1eulem  19971  ablfac1eu  19972  gsumle  20042  pwssplit0  20980  frlmsplit2  21698  mamures  22300  mdetrlin  22505  cnrest  23188  cnpresti  23191  cnprest  23192  ptuncnv  23710  ptunhmeo  23711  ptcmpfi  23716  tsmslem1  24032  tsmssubm  24046  tsmsres  24047  tsmsf1o  24048  tsmsxplem1  24056  tsmsxplem2  24057  psmetres2  24218  xmetres2  24265  metres2  24267  imasdsf1olem  24277  xmetresbl  24341  xrge0gsumle  24738  xrge0tsms  24739  rescncf  24806  mbfres2  25562  limcres  25803  limciun  25811  dvres3  25830  dvmptresicc  25833  dvlip  25914  dvlipcn  25915  dvlip2  25916  dvgt0lem1  25923  dvivthlem1  25929  lhop  25937  ulmres  26313  ulmss  26322  pserdvlem2  26354  jensenlem2  26914  jensen  26915  wlkres  29632  pthdifv  29693  pthdlem1  29729  foresf1o  32466  resf1o  32686  pfxf1  32896  xrge0tsmsd  33028  tocyccntz  33099  elrspunsn  33379  rprmdvdsprod  33484  ply1degltdimlem  33597  zarcmplem  33850  measres  34191  omsmeas  34293  reprsuc  34585  f1resfz0f1d  35089  pfxwlk  35099  pthhashvtx  35103  cvmliftlem6  35265  cvmlift2lem11  35288  satfv1lem  35337  mrsubff1  35489  msubff1  35531  psrbagres  42522  evlselv  42563  fsuppssind  42569  aomclem4  43033  extoimad  44140  imo72b2lem0  44141  imo72b2lem2  44143  imo72b2lem1  44145  imo72b2  44148  wessf1ornlem  45166  feqresmptf  45212  limcperiod  45613  climxlim2  45831  cncfperiod  45864  dirkercncflem4  46091  fourierdlem48  46139  fourierdlem49  46140  fourierdlem51  46142  fourierdlem53  46144  fourierdlem74  46165  fourierdlem75  46166  fourierdlem81  46172  fourierdlem85  46176  fourierdlem88  46179  fourierdlem93  46184  fourierdlem94  46185  fourierdlem95  46186  fourierdlem100  46191  fourierdlem103  46194  fourierdlem104  46195  fourierdlem107  46198  fourierdlem111  46202  fourierdlem112  46203  fourierdlem113  46204  sge0tsms  46365  sge0sup  46376  sge0gerp  46380  sge0pnffigt  46381  sge0lefi  46383  sge0ltfirp  46385  sge0resplit  46391  sge0le  46392  sge0split  46394  sge0iun  46404  meadjun  46447  ismeannd  46452  psmeasurelem  46455  omeunle  46501  omeiunle  46502  caratheodory  46513  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvlelem4  46583  smflimsuplem3  46807  fcoresf1  47057  fcoresfo  47059  lincdifsn  48413