Theorem fssresd 6548

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

Syntax hints:   → wi 4   ⊆ wss 3939   ↾ cres 5560  ⟶wf 6354

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070  df-opab 5132  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-fun 6360  df-fn 6361  df-f 6362

This theorem is referenced by:  feqresmpt  6737  fsuppcor  8870  ramub2  16353  ramub1lem2  16366  funcres  17169  gsumsplit1r  17900  gasubg  18435  gsumzaddlem  19044  dprdfadd  19145  dprdres  19153  dprdf1  19158  dmdprdsplitlem  19162  dmdprdsplit2lem  19170  dmdprdsplit2  19171  dprdsplit  19173  ablfac1eulem  19197  ablfac1eu  19198  pwssplit0  19833  frlmsplit2  20920  mamures  21004  mdetrlin  21214  cnrest  21896  cnpresti  21899  cnprest  21900  ptuncnv  22418  ptunhmeo  22419  ptcmpfi  22424  tsmslem1  22740  tsmssubm  22754  tsmsres  22755  tsmsf1o  22756  tsmsxplem1  22764  tsmsxplem2  22765  psmetres2  22927  xmetres2  22974  metres2  22976  imasdsf1olem  22986  xmetresbl  23050  xrge0gsumle  23444  xrge0tsms  23445  rescncf  23508  mbfres2  24249  limcres  24487  limciun  24495  dvres3  24514  dvlip  24593  dvlipcn  24594  dvlip2  24595  dvgt0lem1  24602  dvivthlem1  24608  lhop  24616  ulmres  24979  ulmss  24988  pserdvlem2  25019  jensenlem2  25568  jensen  25569  wlkres  27455  pthdlem1  27550  foresf1o  30268  resf1o  30469  pfxf1  30622  xrge0tsmsd  30696  gsumle  30729  tocyccntz  30790  measres  31485  omsmeas  31585  reprsuc  31890  f1resfz0f1d  32365  pfxwlk  32374  pthhashvtx  32378  cvmliftlem6  32541  cvmlift2lem11  32564  satfv1lem  32613  mrsubff1  32765  msubff1  32807  aomclem4  39663  extoimad  40521  imo72b2lem0  40522  imo72b2lem2  40524  imo72b2lem1  40527  imo72b2  40531  wessf1ornlem  41451  feqresmptf  41505  limcperiod  41915  climxlim2  42133  cncfperiod  42168  dvmptresicc  42210  dirkercncflem4  42398  fourierdlem48  42446  fourierdlem49  42447  fourierdlem51  42449  fourierdlem53  42451  fourierdlem74  42472  fourierdlem75  42473  fourierdlem81  42479  fourierdlem85  42483  fourierdlem88  42486  fourierdlem93  42491  fourierdlem94  42492  fourierdlem95  42493  fourierdlem100  42498  fourierdlem103  42501  fourierdlem104  42502  fourierdlem107  42505  fourierdlem111  42509  fourierdlem112  42510  fourierdlem113  42511  sge0tsms  42669  sge0sup  42680  sge0gerp  42684  sge0pnffigt  42685  sge0lefi  42687  sge0ltfirp  42689  sge0resplit  42695  sge0le  42696  sge0split  42698  sge0iun  42708  meadjun  42751  ismeannd  42756  psmeasurelem  42759  omeunle  42805  omeiunle  42806  caratheodory  42817  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvlelem4  42887  smflimsuplem3  43103  lincdifsn  44486