Theorem fssresd 6749

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   ↾ cres 5652  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  feqresmpt  6954  resf1extb  7946  resf1ext2b  7947  fsuppcor  9399  f1resfz0f1d  13930  ramub2  17197  ramub1lem2  17210  funcres  18076  gsumsplit1r  18881  gasubg  19521  gsumzaddlem  20140  dprdfadd  20241  dprdres  20249  dprdf1  20254  dmdprdsplitlem  20258  dmdprdsplit2lem  20266  dmdprdsplit2  20267  dprdsplit  20269  ablfac1eulem  20293  ablfac1eu  20294  gsumle  20364  pwssplit0  21338  frlmsplit2  22084  psrbagres  22243  mamures  22717  mdetrlin  22922  cnrest  23608  cnpresti  23611  cnprest  23612  ptuncnv  24131  ptunhmeo  24132  ptcmpfi  24137  tsmslem1  24453  tsmssubm  24467  tsmsres  24468  tsmsf1o  24469  tsmsxplem1  24477  tsmsxplem2  24478  psmetres2  24638  xmetres2  24685  metres2  24687  imasdsf1olem  24697  xmetresbl  24761  xrge0gsumle  25158  xrge0tsms  25159  rescncf  25223  mbfres2  25971  limcres  26211  limciun  26219  dvres3  26238  dvmptresicc  26241  dvlip  26318  dvlipcn  26319  dvlip2  26320  dvgt0lem1  26327  dvivthlem1  26333  lhop  26341  ulmres  26720  ulmss  26729  pserdvlem2  26760  jensenlem2  27320  jensen  27321  wlkres  30254  pfxwlk  30271  pthhashvtx  30320  pthdifv  30321  pthdlem1  30357  foresf1o  33147  resf1o  33368  pfxf1  33555  xrge0tsmsd  33680  tocyccntz  33751  elrspunsn  34025  rprmdvdsprod  34112  evlextv  34220  esplyind  34253  esplyfvn  34255  vietalem  34257  vieta  34258  ply1degltdimlem  34300  zarcmplem  34559  measres  34901  omsmeas  35001  reprsuc  35290  cvmliftlem6  36141  cvmlift2lem11  36164  satfv1lem  36213  mrsubff1  36365  msubff1  36407  evlselv  43710  fsuppssind  43714  aomclem4  44152  extoimad  45257  imo72b2lem0  45258  imo72b2lem2  45260  imo72b2lem1  45262  imo72b2  45265  wessf1ornlem  46293  feqresmptf  46336  limcperiod  46733  climxlim2  46949  cncfperiod  46982  dirkercncflem4  47209  fourierdlem48  47257  fourierdlem49  47258  fourierdlem51  47260  fourierdlem53  47262  fourierdlem74  47283  fourierdlem75  47284  fourierdlem81  47290  fourierdlem85  47294  fourierdlem88  47297  fourierdlem93  47302  fourierdlem94  47303  fourierdlem95  47304  fourierdlem100  47309  fourierdlem103  47312  fourierdlem104  47313  fourierdlem107  47316  fourierdlem111  47320  fourierdlem112  47321  fourierdlem113  47322  sge0tsms  47483  sge0sup  47494  sge0gerp  47498  sge0pnffigt  47499  sge0lefi  47501  sge0ltfirp  47503  sge0resplit  47509  sge0le  47510  sge0split  47512  sge0iun  47522  meadjun  47565  ismeannd  47570  psmeasurelem  47573  omeunle  47619  omeiunle  47620  caratheodory  47631  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  hoidmvlelem4  47701  sssmf  47841  smflimsuplem3  47925  fcoresf1  48232  fcoresfo  48234  lincdifsn  49629