Theorem fssresd 6774

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   ↾ cres 5658  ⟶wf 6557

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-fun 6563  df-fn 6564  df-f 6565

This theorem is used by:  feqresmpt  6980  resf1extb  7973  resf1ext2b  7974  fsuppcor  9426  f1resfz0f1d  13957  ramub2  17224  ramub1lem2  17237  funcres  18103  gsumsplit1r  18908  gasubg  19549  gsumzaddlem  20168  dprdfadd  20269  dprdres  20277  dprdf1  20282  dmdprdsplitlem  20286  dmdprdsplit2lem  20294  dmdprdsplit2  20295  dprdsplit  20297  ablfac1eulem  20321  ablfac1eu  20322  gsumle  20392  pwssplit0  21366  frlmsplit2  22112  psrbagres  22271  mamures  22745  mdetrlin  22950  cnrest  23636  cnpresti  23639  cnprest  23640  ptuncnv  24159  ptunhmeo  24160  ptcmpfi  24165  tsmslem1  24481  tsmssubm  24495  tsmsres  24496  tsmsf1o  24497  tsmsxplem1  24505  tsmsxplem2  24506  psmetres2  24666  xmetres2  24713  metres2  24715  imasdsf1olem  24725  xmetresbl  24789  xrge0gsumle  25186  xrge0tsms  25187  rescncf  25251  mbfres2  25999  limcres  26239  limciun  26247  dvres3  26266  dvmptresicc  26269  dvlip  26346  dvlipcn  26347  dvlip2  26348  dvgt0lem1  26355  dvivthlem1  26361  lhop  26369  ulmres  26748  ulmss  26757  pserdvlem2  26788  jensenlem2  27348  jensen  27349  wlkres  30282  pfxwlk  30299  pthhashvtx  30348  pthdifv  30349  pthdlem1  30385  foresf1o  33175  resf1o  33395  pfxf1  33582  xrge0tsmsd  33710  tocyccntz  33781  elrspunsn  34063  rprmdvdsprod  34150  evlextv  34257  esplyind  34290  esplyfvn  34292  vietalem  34294  vieta  34295  ply1degltdimlem  34337  zarcmplem  34596  measres  34938  omsmeas  35038  reprsuc  35327  cvmliftlem6  36235  cvmlift2lem11  36258  satfv1lem  36307  mrsubff1  36459  msubff1  36501  evlselv  43821  fsuppssind  43825  aomclem4  44263  extoimad  45367  imo72b2lem0  45368  imo72b2lem2  45370  imo72b2lem1  45372  imo72b2  45375  wessf1ornlem  46415  feqresmptf  46458  limcperiod  46855  climxlim2  47071  cncfperiod  47104  dirkercncflem4  47331  fourierdlem48  47379  fourierdlem49  47380  fourierdlem51  47382  fourierdlem53  47384  fourierdlem74  47405  fourierdlem75  47406  fourierdlem81  47412  fourierdlem85  47416  fourierdlem88  47419  fourierdlem93  47424  fourierdlem94  47425  fourierdlem95  47426  fourierdlem100  47431  fourierdlem103  47434  fourierdlem104  47435  fourierdlem107  47438  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  sge0tsms  47605  sge0sup  47616  sge0gerp  47620  sge0pnffigt  47621  sge0lefi  47623  sge0ltfirp  47625  sge0resplit  47631  sge0le  47632  sge0split  47634  sge0iun  47644  meadjun  47687  ismeannd  47692  psmeasurelem  47695  omeunle  47741  omeiunle  47742  caratheodory  47753  hoidmvlelem1  47820  hoidmvlelem2  47821  hoidmvlelem3  47822  hoidmvlelem4  47823  sssmf  47963  smflimsuplem3  48047  fcoresf1  48354  fcoresfo  48356  lincdifsn  49751