Theorem fssresd 6746

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902   ↾ cres 5661  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  feqresmpt  6951  resf1extb  7935  resf1ext2b  7936  fsuppcor  9378  f1resfz0f1d  13852  ramub2  17112  ramub1lem2  17125  funcres  17991  gsumsplit1r  18795  gasubg  19435  gsumzaddlem  20054  dprdfadd  20155  dprdres  20163  dprdf1  20168  dmdprdsplitlem  20172  dmdprdsplit2lem  20180  dmdprdsplit2  20181  dprdsplit  20183  ablfac1eulem  20207  ablfac1eu  20208  gsumle  20278  pwssplit0  21248  frlmsplit2  21992  psrbagres  22151  mamures  22625  mdetrlin  22830  cnrest  23516  cnpresti  23519  cnprest  23520  ptuncnv  24039  ptunhmeo  24040  ptcmpfi  24045  tsmslem1  24361  tsmssubm  24375  tsmsres  24376  tsmsf1o  24377  tsmsxplem1  24385  tsmsxplem2  24386  psmetres2  24546  xmetres2  24593  metres2  24595  imasdsf1olem  24605  xmetresbl  24669  xrge0gsumle  25066  xrge0tsms  25067  rescncf  25131  mbfres2  25879  limcres  26120  limciun  26128  dvres3  26147  dvmptresicc  26150  dvlip  26227  dvlipcn  26228  dvlip2  26229  dvgt0lem1  26236  dvivthlem1  26242  lhop  26250  ulmres  26631  ulmss  26640  pserdvlem2  26671  jensenlem2  27232  jensen  27233  wlkres  30136  pfxwlk  30153  pthhashvtx  30202  pthdifv  30203  pthdlem1  30239  foresf1o  32987  resf1o  33209  pfxf1  33396  xrge0tsmsd  33521  tocyccntz  33592  elrspunsn  33865  rprmdvdsprod  33952  evlextv  34060  esplyind  34093  esplyfvn  34095  vietalem  34097  vieta  34098  ply1degltdimlem  34140  zarcmplem  34399  measres  34741  omsmeas  34842  reprsuc  35131  cvmliftlem6  35877  cvmlift2lem11  35900  satfv1lem  35949  mrsubff1  36101  msubff1  36143  evlselv  43443  fsuppssind  43447  aomclem4  43906  extoimad  45012  imo72b2lem0  45013  imo72b2lem2  45015  imo72b2lem1  45017  imo72b2  45020  wessf1ornlem  46025  feqresmptf  46068  limcperiod  46466  climxlim2  46682  cncfperiod  46715  dirkercncflem4  46942  fourierdlem48  46990  fourierdlem49  46991  fourierdlem51  46993  fourierdlem53  46995  fourierdlem74  47016  fourierdlem75  47017  fourierdlem81  47023  fourierdlem85  47027  fourierdlem88  47030  fourierdlem93  47035  fourierdlem94  47036  fourierdlem95  47037  fourierdlem100  47042  fourierdlem103  47045  fourierdlem104  47046  fourierdlem107  47049  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  sge0tsms  47216  sge0sup  47227  sge0gerp  47231  sge0pnffigt  47232  sge0lefi  47234  sge0ltfirp  47236  sge0resplit  47242  sge0le  47243  sge0split  47245  sge0iun  47255  meadjun  47298  ismeannd  47303  psmeasurelem  47306  omeunle  47352  omeiunle  47353  caratheodory  47364  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  sssmf  47574  smflimsuplem3  47658  fcoresf1  47965  fcoresfo  47967  lincdifsn  49362