Theorem fssresd 6775

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

Syntax hints:   → wi 4   ⊆ wss 3951   ↾ cres 5687  ⟶wf 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-fun 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  feqresmpt  6978  resf1extb  7956  resf1ext2b  7957  fsuppcor  9444  ramub2  17052  ramub1lem2  17065  funcres  17941  gsumsplit1r  18700  gasubg  19320  gsumzaddlem  19939  dprdfadd  20040  dprdres  20048  dprdf1  20053  dmdprdsplitlem  20057  dmdprdsplit2lem  20065  dmdprdsplit2  20066  dprdsplit  20068  ablfac1eulem  20092  ablfac1eu  20093  pwssplit0  21057  frlmsplit2  21793  mamures  22401  mdetrlin  22608  cnrest  23293  cnpresti  23296  cnprest  23297  ptuncnv  23815  ptunhmeo  23816  ptcmpfi  23821  tsmslem1  24137  tsmssubm  24151  tsmsres  24152  tsmsf1o  24153  tsmsxplem1  24161  tsmsxplem2  24162  psmetres2  24324  xmetres2  24371  metres2  24373  imasdsf1olem  24383  xmetresbl  24447  xrge0gsumle  24855  xrge0tsms  24856  rescncf  24923  mbfres2  25680  limcres  25921  limciun  25929  dvres3  25948  dvmptresicc  25951  dvlip  26032  dvlipcn  26033  dvlip2  26034  dvgt0lem1  26041  dvivthlem1  26047  lhop  26055  ulmres  26431  ulmss  26440  pserdvlem2  26472  jensenlem2  27031  jensen  27032  wlkres  29688  pthdifv  29750  pthdlem1  29786  foresf1o  32523  resf1o  32741  pfxf1  32926  xrge0tsmsd  33065  gsumle  33101  tocyccntz  33164  elrspunsn  33457  rprmdvdsprod  33562  ply1degltdimlem  33673  zarcmplem  33880  measres  34223  omsmeas  34325  reprsuc  34630  f1resfz0f1d  35119  pfxwlk  35129  pthhashvtx  35133  cvmliftlem6  35295  cvmlift2lem11  35318  satfv1lem  35367  mrsubff1  35519  msubff1  35561  psrbagres  42556  evlselv  42597  fsuppssind  42603  aomclem4  43069  extoimad  44177  imo72b2lem0  44178  imo72b2lem2  44180  imo72b2lem1  44182  imo72b2  44185  wessf1ornlem  45190  feqresmptf  45236  limcperiod  45643  climxlim2  45861  cncfperiod  45894  dirkercncflem4  46121  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem53  46174  fourierdlem74  46195  fourierdlem75  46196  fourierdlem81  46202  fourierdlem85  46206  fourierdlem88  46209  fourierdlem93  46214  fourierdlem94  46215  fourierdlem95  46216  fourierdlem100  46221  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  sge0tsms  46395  sge0sup  46406  sge0gerp  46410  sge0pnffigt  46411  sge0lefi  46413  sge0ltfirp  46415  sge0resplit  46421  sge0le  46422  sge0split  46424  sge0iun  46434  meadjun  46477  ismeannd  46482  psmeasurelem  46485  omeunle  46531  omeiunle  46532  caratheodory  46543  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  smflimsuplem3  46837  fcoresf1  47081  fcoresfo  47083  lincdifsn  48341