Theorem fssresd 6745

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

Syntax hints:   → wi 4   ⊆ wss 3926   ↾ cres 5656  ⟶wf 6527

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-fun 6533  df-fn 6534  df-f 6535

This theorem is referenced by:  feqresmpt  6948  resf1extb  7930  resf1ext2b  7931  fsuppcor  9416  ramub2  17034  ramub1lem2  17047  funcres  17909  gsumsplit1r  18665  gasubg  19285  gsumzaddlem  19902  dprdfadd  20003  dprdres  20011  dprdf1  20016  dmdprdsplitlem  20020  dmdprdsplit2lem  20028  dmdprdsplit2  20029  dprdsplit  20031  ablfac1eulem  20055  ablfac1eu  20056  pwssplit0  21016  frlmsplit2  21733  mamures  22335  mdetrlin  22540  cnrest  23223  cnpresti  23226  cnprest  23227  ptuncnv  23745  ptunhmeo  23746  ptcmpfi  23751  tsmslem1  24067  tsmssubm  24081  tsmsres  24082  tsmsf1o  24083  tsmsxplem1  24091  tsmsxplem2  24092  psmetres2  24253  xmetres2  24300  metres2  24302  imasdsf1olem  24312  xmetresbl  24376  xrge0gsumle  24773  xrge0tsms  24774  rescncf  24841  mbfres2  25598  limcres  25839  limciun  25847  dvres3  25866  dvmptresicc  25869  dvlip  25950  dvlipcn  25951  dvlip2  25952  dvgt0lem1  25959  dvivthlem1  25965  lhop  25973  ulmres  26349  ulmss  26358  pserdvlem2  26390  jensenlem2  26950  jensen  26951  wlkres  29650  pthdifv  29712  pthdlem1  29748  foresf1o  32485  resf1o  32707  pfxf1  32917  xrge0tsmsd  33056  gsumle  33092  tocyccntz  33155  elrspunsn  33444  rprmdvdsprod  33549  ply1degltdimlem  33662  zarcmplem  33912  measres  34253  omsmeas  34355  reprsuc  34647  f1resfz0f1d  35136  pfxwlk  35146  pthhashvtx  35150  cvmliftlem6  35312  cvmlift2lem11  35335  satfv1lem  35384  mrsubff1  35536  msubff1  35578  psrbagres  42569  evlselv  42610  fsuppssind  42616  aomclem4  43081  extoimad  44188  imo72b2lem0  44189  imo72b2lem2  44191  imo72b2lem1  44193  imo72b2  44196  wessf1ornlem  45209  feqresmptf  45255  limcperiod  45657  climxlim2  45875  cncfperiod  45908  dirkercncflem4  46135  fourierdlem48  46183  fourierdlem49  46184  fourierdlem51  46186  fourierdlem53  46188  fourierdlem74  46209  fourierdlem75  46210  fourierdlem81  46216  fourierdlem85  46220  fourierdlem88  46223  fourierdlem93  46228  fourierdlem94  46229  fourierdlem95  46230  fourierdlem100  46235  fourierdlem103  46238  fourierdlem104  46239  fourierdlem107  46242  fourierdlem111  46246  fourierdlem112  46247  fourierdlem113  46248  sge0tsms  46409  sge0sup  46420  sge0gerp  46424  sge0pnffigt  46425  sge0lefi  46427  sge0ltfirp  46429  sge0resplit  46435  sge0le  46436  sge0split  46438  sge0iun  46448  meadjun  46491  ismeannd  46496  psmeasurelem  46499  omeunle  46545  omeiunle  46546  caratheodory  46557  hoidmvlelem1  46624  hoidmvlelem2  46625  hoidmvlelem3  46626  hoidmvlelem4  46627  smflimsuplem3  46851  fcoresf1  47098  fcoresfo  47100  lincdifsn  48400