Theorem fssresd 6741

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   ↾ cres 5653  ⟶wf 6527

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  feqresmpt  6946  resf1extb  7935  resf1ext2b  7936  fsuppcor  9380  f1resfz0f1d  13907  ramub2  17172  ramub1lem2  17185  funcres  18051  gsumsplit1r  18856  gasubg  19496  gsumzaddlem  20115  dprdfadd  20216  dprdres  20224  dprdf1  20229  dmdprdsplitlem  20233  dmdprdsplit2lem  20241  dmdprdsplit2  20242  dprdsplit  20244  ablfac1eulem  20268  ablfac1eu  20269  gsumle  20339  pwssplit0  21313  frlmsplit2  22059  psrbagres  22218  mamures  22692  mdetrlin  22897  cnrest  23583  cnpresti  23586  cnprest  23587  ptuncnv  24106  ptunhmeo  24107  ptcmpfi  24112  tsmslem1  24428  tsmssubm  24442  tsmsres  24443  tsmsf1o  24444  tsmsxplem1  24452  tsmsxplem2  24453  psmetres2  24613  xmetres2  24660  metres2  24662  imasdsf1olem  24672  xmetresbl  24736  xrge0gsumle  25133  xrge0tsms  25134  rescncf  25198  mbfres2  25946  limcres  26186  limciun  26194  dvres3  26213  dvmptresicc  26216  dvlip  26293  dvlipcn  26294  dvlip2  26295  dvgt0lem1  26302  dvivthlem1  26308  lhop  26316  ulmres  26697  ulmss  26706  pserdvlem2  26737  jensenlem2  27297  jensen  27298  wlkres  30231  pfxwlk  30248  pthhashvtx  30297  pthdifv  30298  pthdlem1  30334  foresf1o  33082  resf1o  33304  pfxf1  33491  xrge0tsmsd  33616  tocyccntz  33687  elrspunsn  33961  rprmdvdsprod  34048  evlextv  34156  esplyind  34189  esplyfvn  34191  vietalem  34193  vieta  34194  ply1degltdimlem  34236  zarcmplem  34495  measres  34837  omsmeas  34938  reprsuc  35227  cvmliftlem6  36024  cvmlift2lem11  36047  satfv1lem  36096  mrsubff1  36248  msubff1  36290  evlselv  43579  fsuppssind  43583  aomclem4  44017  extoimad  45123  imo72b2lem0  45124  imo72b2lem2  45126  imo72b2lem1  45128  imo72b2  45131  wessf1ornlem  46143  feqresmptf  46186  limcperiod  46584  climxlim2  46800  cncfperiod  46833  dirkercncflem4  47060  fourierdlem48  47108  fourierdlem49  47109  fourierdlem51  47111  fourierdlem53  47113  fourierdlem74  47134  fourierdlem75  47135  fourierdlem81  47141  fourierdlem85  47145  fourierdlem88  47148  fourierdlem93  47153  fourierdlem94  47154  fourierdlem95  47155  fourierdlem100  47160  fourierdlem103  47163  fourierdlem104  47164  fourierdlem107  47167  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  sge0tsms  47334  sge0sup  47345  sge0gerp  47349  sge0pnffigt  47350  sge0lefi  47352  sge0ltfirp  47354  sge0resplit  47360  sge0le  47361  sge0split  47363  sge0iun  47373  meadjun  47416  ismeannd  47421  psmeasurelem  47424  omeunle  47470  omeiunle  47471  caratheodory  47482  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  sssmf  47692  smflimsuplem3  47776  fcoresf1  48083  fcoresfo  48085  lincdifsn  49480