Theorem fssresd 6735

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

Syntax hints:   → wi 4   ⊆ wss 3907   ↾ cres 5653  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  feqresmpt  6940  resf1extb  7919  resf1ext2b  7920  fsuppcor  9352  ramub2  17062  ramub1lem2  17075  funcres  17941  gsumsplit1r  18733  gasubg  19360  gsumzaddlem  19979  dprdfadd  20080  dprdres  20088  dprdf1  20093  dmdprdsplitlem  20097  dmdprdsplit2lem  20105  dmdprdsplit2  20106  dprdsplit  20108  ablfac1eulem  20132  ablfac1eu  20133  gsumle  20203  pwssplit0  21145  frlmsplit2  21880  psrbagres  22037  mamures  22511  mdetrlin  22716  cnrest  23399  cnpresti  23402  cnprest  23403  ptuncnv  23921  ptunhmeo  23922  ptcmpfi  23927  tsmslem1  24243  tsmssubm  24257  tsmsres  24258  tsmsf1o  24259  tsmsxplem1  24267  tsmsxplem2  24268  psmetres2  24428  xmetres2  24475  metres2  24477  imasdsf1olem  24487  xmetresbl  24551  xrge0gsumle  24948  xrge0tsms  24949  rescncf  25013  mbfres2  25761  limcres  26002  limciun  26010  dvres3  26029  dvmptresicc  26032  dvlip  26109  dvlipcn  26110  dvlip2  26111  dvgt0lem1  26118  dvivthlem1  26124  lhop  26132  ulmres  26505  ulmss  26514  pserdvlem2  26545  jensenlem2  27106  jensen  27107  wlkres  29923  pthdifv  29984  pthdlem1  30020  foresf1o  32756  resf1o  32983  pfxf1  33170  xrge0tsmsd  33301  tocyccntz  33372  elrspunsn  33648  rprmdvdsprod  33736  extvfvvcl  33837  extvfvcl  33838  evlextv  33844  esplyind  33877  esplyfvn  33879  vietalem  33881  vieta  33882  ply1degltdimlem  33924  zarcmplem  34183  measres  34524  omsmeas  34625  reprsuc  34914  f1resfz0f1d  35471  pfxwlk  35482  pthhashvtx  35486  cvmliftlem6  35648  cvmlift2lem11  35671  satfv1lem  35720  mrsubff1  35872  msubff1  35914  evlselv  43178  fsuppssind  43182  aomclem4  43641  extoimad  44747  imo72b2lem0  44748  imo72b2lem2  44750  imo72b2lem1  44752  imo72b2  44755  wessf1ornlem  45762  feqresmptf  45805  limcperiod  46203  climxlim2  46419  cncfperiod  46452  dirkercncflem4  46679  fourierdlem48  46727  fourierdlem49  46728  fourierdlem51  46730  fourierdlem53  46732  fourierdlem74  46753  fourierdlem75  46754  fourierdlem81  46760  fourierdlem85  46764  fourierdlem88  46767  fourierdlem93  46772  fourierdlem94  46773  fourierdlem95  46774  fourierdlem100  46779  fourierdlem103  46782  fourierdlem104  46783  fourierdlem107  46786  fourierdlem111  46790  fourierdlem112  46791  fourierdlem113  46792  sge0tsms  46953  sge0sup  46964  sge0gerp  46968  sge0pnffigt  46969  sge0lefi  46971  sge0ltfirp  46973  sge0resplit  46979  sge0le  46980  sge0split  46982  sge0iun  46992  meadjun  47035  ismeannd  47040  psmeasurelem  47043  omeunle  47089  omeiunle  47090  caratheodory  47101  hoidmvlelem1  47168  hoidmvlelem2  47169  hoidmvlelem3  47170  hoidmvlelem4  47171  sssmf  47311  smflimsuplem3  47395  fcoresf1  47662  fcoresfo  47664  lincdifsn  49056