Theorem fssresd 6745

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3904   ↾ cres 5662  ⟶wf 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-fun 6538  df-fn 6539  df-f 6540

This theorem is used by:  feqresmpt  6950  resf1extb  7929  resf1ext2b  7930  fsuppcor  9362  ramub2  17080  ramub1lem2  17093  funcres  17959  gsumsplit1r  18751  gasubg  19378  gsumzaddlem  19997  dprdfadd  20098  dprdres  20106  dprdf1  20111  dmdprdsplitlem  20115  dmdprdsplit2lem  20123  dmdprdsplit2  20124  dprdsplit  20126  ablfac1eulem  20150  ablfac1eu  20151  gsumle  20221  pwssplit0  21190  frlmsplit2  21934  psrbagres  22091  mamures  22565  mdetrlin  22770  cnrest  23453  cnpresti  23456  cnprest  23457  ptuncnv  23975  ptunhmeo  23976  ptcmpfi  23981  tsmslem1  24297  tsmssubm  24311  tsmsres  24312  tsmsf1o  24313  tsmsxplem1  24321  tsmsxplem2  24322  psmetres2  24482  xmetres2  24529  metres2  24531  imasdsf1olem  24541  xmetresbl  24605  xrge0gsumle  25002  xrge0tsms  25003  rescncf  25067  mbfres2  25815  limcres  26056  limciun  26064  dvres3  26083  dvmptresicc  26086  dvlip  26163  dvlipcn  26164  dvlip2  26165  dvgt0lem1  26172  dvivthlem1  26178  lhop  26186  ulmres  26562  ulmss  26571  pserdvlem2  26602  jensenlem2  27163  jensen  27164  wlkres  30029  pthdifv  30090  pthdlem1  30126  foresf1o  32861  resf1o  33086  pfxf1  33273  xrge0tsmsd  33402  tocyccntz  33473  elrspunsn  33746  rprmdvdsprod  33833  extvfvvcl  33934  extvfvcl  33935  evlextv  33941  esplyind  33974  esplyfvn  33976  vietalem  33978  vieta  33979  ply1degltdimlem  34021  zarcmplem  34280  measres  34621  omsmeas  34722  reprsuc  35011  f1resfz0f1d  35613  pfxwlk  35624  pthhashvtx  35628  cvmliftlem6  35790  cvmlift2lem11  35813  satfv1lem  35862  mrsubff1  36014  msubff1  36056  evlselv  43349  fsuppssind  43353  aomclem4  43812  extoimad  44918  imo72b2lem0  44919  imo72b2lem2  44921  imo72b2lem1  44923  imo72b2  44926  wessf1ornlem  45931  feqresmptf  45974  limcperiod  46372  climxlim2  46588  cncfperiod  46621  dirkercncflem4  46848  fourierdlem48  46896  fourierdlem49  46897  fourierdlem51  46899  fourierdlem53  46901  fourierdlem74  46922  fourierdlem75  46923  fourierdlem81  46929  fourierdlem85  46933  fourierdlem88  46936  fourierdlem93  46941  fourierdlem94  46942  fourierdlem95  46943  fourierdlem100  46948  fourierdlem103  46951  fourierdlem104  46952  fourierdlem107  46955  fourierdlem111  46959  fourierdlem112  46960  fourierdlem113  46961  sge0tsms  47122  sge0sup  47133  sge0gerp  47137  sge0pnffigt  47138  sge0lefi  47140  sge0ltfirp  47142  sge0resplit  47148  sge0le  47149  sge0split  47151  sge0iun  47161  meadjun  47204  ismeannd  47209  psmeasurelem  47212  omeunle  47258  omeiunle  47259  caratheodory  47270  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvlelem4  47340  sssmf  47480  smflimsuplem3  47564  fcoresf1  47834  fcoresfo  47836  lincdifsn  49232