Theorem fssresd 6752

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908   ↾ cres 5668  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  feqresmpt  6957  resf1extb  7940  resf1ext2b  7941  fsuppcor  9374  f1resfz0f1d  13840  ramub2  17099  ramub1lem2  17112  funcres  17978  gsumsplit1r  18774  gasubg  19403  gsumzaddlem  20022  dprdfadd  20123  dprdres  20131  dprdf1  20136  dmdprdsplitlem  20140  dmdprdsplit2lem  20148  dmdprdsplit2  20149  dprdsplit  20151  ablfac1eulem  20175  ablfac1eu  20176  gsumle  20246  pwssplit0  21216  frlmsplit2  21960  psrbagres  22117  mamures  22591  mdetrlin  22796  cnrest  23479  cnpresti  23482  cnprest  23483  ptuncnv  24001  ptunhmeo  24002  ptcmpfi  24007  tsmslem1  24323  tsmssubm  24337  tsmsres  24338  tsmsf1o  24339  tsmsxplem1  24347  tsmsxplem2  24348  psmetres2  24508  xmetres2  24555  metres2  24557  imasdsf1olem  24567  xmetresbl  24631  xrge0gsumle  25028  xrge0tsms  25029  rescncf  25093  mbfres2  25841  limcres  26082  limciun  26090  dvres3  26109  dvmptresicc  26112  dvlip  26189  dvlipcn  26190  dvlip2  26191  dvgt0lem1  26198  dvivthlem1  26204  lhop  26212  ulmres  26588  ulmss  26597  pserdvlem2  26628  jensenlem2  27189  jensen  27190  wlkres  30055  pthdifv  30116  pthdlem1  30152  foresf1o  32887  resf1o  33112  pfxf1  33299  xrge0tsmsd  33424  tocyccntz  33495  elrspunsn  33768  rprmdvdsprod  33855  extvfvvcl  33956  extvfvcl  33957  evlextv  33963  esplyind  33996  esplyfvn  33998  vietalem  34000  vieta  34001  ply1degltdimlem  34043  zarcmplem  34302  measres  34644  omsmeas  34745  reprsuc  35034  pfxwlk  35637  pthhashvtx  35641  cvmliftlem6  35803  cvmlift2lem11  35826  satfv1lem  35875  mrsubff1  36027  msubff1  36069  evlselv  43362  fsuppssind  43366  aomclem4  43825  extoimad  44931  imo72b2lem0  44932  imo72b2lem2  44934  imo72b2lem1  44936  imo72b2  44939  wessf1ornlem  45944  feqresmptf  45987  limcperiod  46385  climxlim2  46601  cncfperiod  46634  dirkercncflem4  46861  fourierdlem48  46909  fourierdlem49  46910  fourierdlem51  46912  fourierdlem53  46914  fourierdlem74  46935  fourierdlem75  46936  fourierdlem81  46942  fourierdlem85  46946  fourierdlem88  46949  fourierdlem93  46954  fourierdlem94  46955  fourierdlem95  46956  fourierdlem100  46961  fourierdlem103  46964  fourierdlem104  46965  fourierdlem107  46968  fourierdlem111  46972  fourierdlem112  46973  fourierdlem113  46974  sge0tsms  47135  sge0sup  47146  sge0gerp  47150  sge0pnffigt  47151  sge0lefi  47153  sge0ltfirp  47155  sge0resplit  47161  sge0le  47162  sge0split  47164  sge0iun  47174  meadjun  47217  ismeannd  47222  psmeasurelem  47225  omeunle  47271  omeiunle  47272  caratheodory  47283  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem4  47353  sssmf  47493  smflimsuplem3  47577  fcoresf1  47847  fcoresfo  47849  lincdifsn  49245