Theorem fssresd 6697

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

Syntax hints:   → wi 4   ⊆ wss 3898   ↾ cres 5623  ⟶wf 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-fun 6490  df-fn 6491  df-f 6492

This theorem is referenced by:  feqresmpt  6899  resf1extb  7872  resf1ext2b  7873  fsuppcor  9297  ramub2  16930  ramub1lem2  16943  funcres  17807  gsumsplit1r  18599  gasubg  19218  gsumzaddlem  19837  dprdfadd  19938  dprdres  19946  dprdf1  19951  dmdprdsplitlem  19955  dmdprdsplit2lem  19963  dmdprdsplit2  19964  dprdsplit  19966  ablfac1eulem  19990  ablfac1eu  19991  gsumle  20061  pwssplit0  20996  frlmsplit2  21714  mamures  22315  mdetrlin  22520  cnrest  23203  cnpresti  23206  cnprest  23207  ptuncnv  23725  ptunhmeo  23726  ptcmpfi  23731  tsmslem1  24047  tsmssubm  24061  tsmsres  24062  tsmsf1o  24063  tsmsxplem1  24071  tsmsxplem2  24072  psmetres2  24232  xmetres2  24279  metres2  24281  imasdsf1olem  24291  xmetresbl  24355  xrge0gsumle  24752  xrge0tsms  24753  rescncf  24820  mbfres2  25576  limcres  25817  limciun  25825  dvres3  25844  dvmptresicc  25847  dvlip  25928  dvlipcn  25929  dvlip2  25930  dvgt0lem1  25937  dvivthlem1  25943  lhop  25951  ulmres  26327  ulmss  26336  pserdvlem2  26368  jensenlem2  26928  jensen  26929  wlkres  29651  pthdifv  29712  pthdlem1  29748  foresf1o  32488  resf1o  32719  pfxf1  32932  xrge0tsmsd  33051  tocyccntz  33122  elrspunsn  33403  rprmdvdsprod  33508  extvfvvcl  33588  extvfvcl  33589  esplyind  33615  ply1degltdimlem  33658  zarcmplem  33917  measres  34258  omsmeas  34359  reprsuc  34651  f1resfz0f1d  35181  pfxwlk  35191  pthhashvtx  35195  cvmliftlem6  35357  cvmlift2lem11  35380  satfv1lem  35429  mrsubff1  35581  msubff1  35623  psrbagres  42667  evlselv  42708  fsuppssind  42714  aomclem4  43177  extoimad  44284  imo72b2lem0  44285  imo72b2lem2  44287  imo72b2lem1  44289  imo72b2  44292  wessf1ornlem  45309  feqresmptf  45355  limcperiod  45755  climxlim2  45971  cncfperiod  46004  dirkercncflem4  46231  fourierdlem48  46279  fourierdlem49  46280  fourierdlem51  46282  fourierdlem53  46284  fourierdlem74  46305  fourierdlem75  46306  fourierdlem81  46312  fourierdlem85  46316  fourierdlem88  46319  fourierdlem93  46324  fourierdlem94  46325  fourierdlem95  46326  fourierdlem100  46331  fourierdlem103  46334  fourierdlem104  46335  fourierdlem107  46338  fourierdlem111  46342  fourierdlem112  46343  fourierdlem113  46344  sge0tsms  46505  sge0sup  46516  sge0gerp  46520  sge0pnffigt  46521  sge0lefi  46523  sge0ltfirp  46525  sge0resplit  46531  sge0le  46532  sge0split  46534  sge0iun  46544  meadjun  46587  ismeannd  46592  psmeasurelem  46595  omeunle  46641  omeiunle  46642  caratheodory  46653  hoidmvlelem1  46720  hoidmvlelem2  46721  hoidmvlelem3  46722  hoidmvlelem4  46723  smflimsuplem3  46947  fcoresf1  47196  fcoresfo  47198  lincdifsn  48552