Theorem fssresd 6321

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

Syntax hints:   → wi 4   ⊆ wss 3792   ↾ cres 5357  ⟶wf 6131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-fun 6137  df-fn 6138  df-f 6139

This theorem is referenced by:  feqresmpt  6510  fsuppcor  8597  ramub2  16122  ramub1lem2  16135  funcres  16941  gasubg  18118  gsumzaddlem  18707  dprdfadd  18806  dprdres  18814  dprdf1  18819  dmdprdsplitlem  18823  dmdprdsplit2lem  18831  dmdprdsplit2  18832  dprdsplit  18834  ablfac1eulem  18858  ablfac1eu  18859  pwssplit0  19453  frlmsplit2  20516  mamures  20600  mdetrlin  20813  cnrest  21497  cnpresti  21500  cnprest  21501  ptuncnv  22019  ptunhmeo  22020  ptcmpfi  22025  tsmslem1  22340  tsmssubm  22354  tsmsres  22355  tsmsf1o  22356  tsmsxplem1  22364  tsmsxplem2  22365  psmetres2  22527  xmetres2  22574  metres2  22576  imasdsf1olem  22586  xmetresbl  22650  xrge0gsumle  23044  xrge0tsms  23045  rescncf  23108  mbfres2  23849  limcres  24087  limciun  24095  dvres3  24114  dvlip  24193  dvlipcn  24194  dvlip2  24195  dvgt0lem1  24202  dvivthlem1  24208  lhop  24216  ulmres  24579  ulmss  24588  pserdvlem2  24619  jensenlem2  25166  jensen  25167  wlkres  27019  wlkresOLD  27021  pthdlem1  27118  foresf1o  29905  resf1o  30071  gsumle  30341  xrge0tsmsd  30347  measres  30883  omsmeas  30983  reprsuc  31295  cvmliftlem6  31871  cvmlift2lem11  31894  mrsubff1  32010  msubff1  32052  aomclem4  38590  extoimad  39424  imo72b2lem0  39425  imo72b2lem2  39427  imo72b2lem1  39431  imo72b2  39435  wessf1ornlem  40298  feqresmptf  40354  limcperiod  40772  climxlim2  40990  cncfperiod  41024  dvmptresicc  41066  dirkercncflem4  41254  fourierdlem48  41302  fourierdlem49  41303  fourierdlem51  41305  fourierdlem53  41307  fourierdlem74  41328  fourierdlem75  41329  fourierdlem81  41335  fourierdlem85  41339  fourierdlem88  41342  fourierdlem93  41347  fourierdlem94  41348  fourierdlem95  41349  fourierdlem100  41354  fourierdlem103  41357  fourierdlem104  41358  fourierdlem107  41361  fourierdlem111  41365  fourierdlem112  41366  fourierdlem113  41367  sge0tsms  41525  sge0sup  41536  sge0gerp  41540  sge0pnffigt  41541  sge0lefi  41543  sge0ltfirp  41545  sge0resplit  41551  sge0le  41552  sge0split  41554  sge0iun  41564  meadjun  41607  ismeannd  41612  psmeasurelem  41615  omeunle  41661  omeiunle  41662  caratheodory  41673  hoidmvlelem1  41740  hoidmvlelem2  41741  hoidmvlelem3  41742  hoidmvlelem4  41743  smflimsuplem3  41959  lincdifsn  43232