Theorem fssresd 6776

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

Syntax hints:   → wi 4   ⊆ wss 3963   ↾ cres 5691  ⟶wf 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-fun 6565  df-fn 6566  df-f 6567

This theorem is referenced by:  feqresmpt  6978  fsuppcor  9442  ramub2  17048  ramub1lem2  17061  funcres  17947  gsumsplit1r  18713  gasubg  19333  gsumzaddlem  19954  dprdfadd  20055  dprdres  20063  dprdf1  20068  dmdprdsplitlem  20072  dmdprdsplit2lem  20080  dmdprdsplit2  20081  dprdsplit  20083  ablfac1eulem  20107  ablfac1eu  20108  pwssplit0  21075  frlmsplit2  21811  mamures  22417  mdetrlin  22624  cnrest  23309  cnpresti  23312  cnprest  23313  ptuncnv  23831  ptunhmeo  23832  ptcmpfi  23837  tsmslem1  24153  tsmssubm  24167  tsmsres  24168  tsmsf1o  24169  tsmsxplem1  24177  tsmsxplem2  24178  psmetres2  24340  xmetres2  24387  metres2  24389  imasdsf1olem  24399  xmetresbl  24463  xrge0gsumle  24869  xrge0tsms  24870  rescncf  24937  mbfres2  25694  limcres  25936  limciun  25944  dvres3  25963  dvmptresicc  25966  dvlip  26047  dvlipcn  26048  dvlip2  26049  dvgt0lem1  26056  dvivthlem1  26062  lhop  26070  ulmres  26446  ulmss  26455  pserdvlem2  26487  jensenlem2  27046  jensen  27047  wlkres  29703  pthdlem1  29799  foresf1o  32532  resf1o  32748  pfxf1  32911  xrge0tsmsd  33048  gsumle  33084  tocyccntz  33147  elrspunsn  33437  rprmdvdsprod  33542  ply1degltdimlem  33650  zarcmplem  33842  measres  34203  omsmeas  34305  reprsuc  34609  f1resfz0f1d  35098  pfxwlk  35108  pthhashvtx  35112  cvmliftlem6  35275  cvmlift2lem11  35298  satfv1lem  35347  mrsubff1  35499  msubff1  35541  psrbagres  42533  evlselv  42574  fsuppssind  42580  aomclem4  43046  extoimad  44154  imo72b2lem0  44155  imo72b2lem2  44157  imo72b2lem1  44159  imo72b2  44162  wessf1ornlem  45128  feqresmptf  45174  limcperiod  45584  climxlim2  45802  cncfperiod  45835  dirkercncflem4  46062  fourierdlem48  46110  fourierdlem49  46111  fourierdlem51  46113  fourierdlem53  46115  fourierdlem74  46136  fourierdlem75  46137  fourierdlem81  46143  fourierdlem85  46147  fourierdlem88  46150  fourierdlem93  46155  fourierdlem94  46156  fourierdlem95  46157  fourierdlem100  46162  fourierdlem103  46165  fourierdlem104  46166  fourierdlem107  46169  fourierdlem111  46173  fourierdlem112  46174  fourierdlem113  46175  sge0tsms  46336  sge0sup  46347  sge0gerp  46351  sge0pnffigt  46352  sge0lefi  46354  sge0ltfirp  46356  sge0resplit  46362  sge0le  46363  sge0split  46365  sge0iun  46375  meadjun  46418  ismeannd  46423  psmeasurelem  46426  omeunle  46472  omeiunle  46473  caratheodory  46484  hoidmvlelem1  46551  hoidmvlelem2  46552  hoidmvlelem3  46553  hoidmvlelem4  46554  smflimsuplem3  46778  fcoresf1  47019  fcoresfo  47021  lincdifsn  48270