Theorem fssresd 6755

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

Syntax hints:   → wi 4   ⊆ wss 3947   ↾ cres 5677  ⟶wf 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-fun 6542  df-fn 6543  df-f 6544

This theorem is referenced by:  feqresmpt  6958  fsuppcor  9395  ramub2  16943  ramub1lem2  16956  funcres  17842  gsumsplit1r  18602  gasubg  19160  gsumzaddlem  19783  dprdfadd  19884  dprdres  19892  dprdf1  19897  dmdprdsplitlem  19901  dmdprdsplit2lem  19909  dmdprdsplit2  19910  dprdsplit  19912  ablfac1eulem  19936  ablfac1eu  19937  pwssplit0  20661  frlmsplit2  21319  mamures  21883  mdetrlin  22095  cnrest  22780  cnpresti  22783  cnprest  22784  ptuncnv  23302  ptunhmeo  23303  ptcmpfi  23308  tsmslem1  23624  tsmssubm  23638  tsmsres  23639  tsmsf1o  23640  tsmsxplem1  23648  tsmsxplem2  23649  psmetres2  23811  xmetres2  23858  metres2  23860  imasdsf1olem  23870  xmetresbl  23934  xrge0gsumle  24340  xrge0tsms  24341  rescncf  24404  mbfres2  25153  limcres  25394  limciun  25402  dvres3  25421  dvmptresicc  25424  dvlip  25501  dvlipcn  25502  dvlip2  25503  dvgt0lem1  25510  dvivthlem1  25516  lhop  25524  ulmres  25891  ulmss  25900  pserdvlem2  25931  jensenlem2  26481  jensen  26482  wlkres  28916  pthdlem1  29012  foresf1o  31729  resf1o  31942  pfxf1  32095  xrge0tsmsd  32196  gsumle  32229  tocyccntz  32290  elrspunsn  32535  ply1degltdimlem  32695  zarcmplem  32849  measres  33208  omsmeas  33310  reprsuc  33615  f1resfz0f1d  34091  pfxwlk  34102  pthhashvtx  34106  cvmliftlem6  34269  cvmlift2lem11  34292  satfv1lem  34341  mrsubff1  34493  msubff1  34535  psrbagres  41112  evlselv  41156  fsuppssind  41162  aomclem4  41784  extoimad  42901  imo72b2lem0  42902  imo72b2lem2  42904  imo72b2lem1  42906  imo72b2  42909  wessf1ornlem  43867  feqresmptf  43916  limcperiod  44330  climxlim2  44548  cncfperiod  44581  dirkercncflem4  44808  fourierdlem48  44856  fourierdlem49  44857  fourierdlem51  44859  fourierdlem53  44861  fourierdlem74  44882  fourierdlem75  44883  fourierdlem81  44889  fourierdlem85  44893  fourierdlem88  44896  fourierdlem93  44901  fourierdlem94  44902  fourierdlem95  44903  fourierdlem100  44908  fourierdlem103  44911  fourierdlem104  44912  fourierdlem107  44915  fourierdlem111  44919  fourierdlem112  44920  fourierdlem113  44921  sge0tsms  45082  sge0sup  45093  sge0gerp  45097  sge0pnffigt  45098  sge0lefi  45100  sge0ltfirp  45102  sge0resplit  45108  sge0le  45109  sge0split  45111  sge0iun  45121  meadjun  45164  ismeannd  45169  psmeasurelem  45172  omeunle  45218  omeiunle  45219  caratheodory  45230  hoidmvlelem1  45297  hoidmvlelem2  45298  hoidmvlelem3  45299  hoidmvlelem4  45300  smflimsuplem3  45524  fcoresf1  45765  fcoresfo  45767  lincdifsn  47058