Theorem fssresd 6539

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

Syntax hints:   → wi 4   ⊆ wss 3935   ↾ cres 5551  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-fun 6351  df-fn 6352  df-f 6353

This theorem is referenced by:  feqresmpt  6728  fsuppcor  8861  ramub2  16344  ramub1lem2  16357  funcres  17160  gsumsplit1r  17891  gasubg  18426  gsumzaddlem  19035  dprdfadd  19136  dprdres  19144  dprdf1  19149  dmdprdsplitlem  19153  dmdprdsplit2lem  19161  dmdprdsplit2  19162  dprdsplit  19164  ablfac1eulem  19188  ablfac1eu  19189  pwssplit0  19824  frlmsplit2  20911  mamures  20995  mdetrlin  21205  cnrest  21887  cnpresti  21890  cnprest  21891  ptuncnv  22409  ptunhmeo  22410  ptcmpfi  22415  tsmslem1  22731  tsmssubm  22745  tsmsres  22746  tsmsf1o  22747  tsmsxplem1  22755  tsmsxplem2  22756  psmetres2  22918  xmetres2  22965  metres2  22967  imasdsf1olem  22977  xmetresbl  23041  xrge0gsumle  23435  xrge0tsms  23436  rescncf  23499  mbfres2  24240  limcres  24478  limciun  24486  dvres3  24505  dvlip  24584  dvlipcn  24585  dvlip2  24586  dvgt0lem1  24593  dvivthlem1  24599  lhop  24607  ulmres  24970  ulmss  24979  pserdvlem2  25010  jensenlem2  25559  jensen  25560  wlkres  27446  pthdlem1  27541  foresf1o  30259  resf1o  30460  pfxf1  30613  xrge0tsmsd  30687  gsumle  30720  tocyccntz  30781  measres  31476  omsmeas  31576  reprsuc  31881  f1resfz0f1d  32356  pfxwlk  32365  pthhashvtx  32369  cvmliftlem6  32532  cvmlift2lem11  32555  satfv1lem  32604  mrsubff1  32756  msubff1  32798  aomclem4  39650  extoimad  40508  imo72b2lem0  40509  imo72b2lem2  40511  imo72b2lem1  40514  imo72b2  40518  wessf1ornlem  41438  feqresmptf  41492  limcperiod  41902  climxlim2  42120  cncfperiod  42155  dvmptresicc  42197  dirkercncflem4  42385  fourierdlem48  42433  fourierdlem49  42434  fourierdlem51  42436  fourierdlem53  42438  fourierdlem74  42459  fourierdlem75  42460  fourierdlem81  42466  fourierdlem85  42470  fourierdlem88  42473  fourierdlem93  42478  fourierdlem94  42479  fourierdlem95  42480  fourierdlem100  42485  fourierdlem103  42488  fourierdlem104  42489  fourierdlem107  42492  fourierdlem111  42496  fourierdlem112  42497  fourierdlem113  42498  sge0tsms  42656  sge0sup  42667  sge0gerp  42671  sge0pnffigt  42672  sge0lefi  42674  sge0ltfirp  42676  sge0resplit  42682  sge0le  42683  sge0split  42685  sge0iun  42695  meadjun  42738  ismeannd  42743  psmeasurelem  42746  omeunle  42792  omeiunle  42793  caratheodory  42804  hoidmvlelem1  42871  hoidmvlelem2  42872  hoidmvlelem3  42873  hoidmvlelem4  42874  smflimsuplem3  43090  lincdifsn  44473