Theorem fssresd 6727

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

Syntax hints:   → wi 4   ⊆ wss 3914   ↾ cres 5640  ⟶wf 6507

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  feqresmpt  6930  resf1extb  7910  resf1ext2b  7911  fsuppcor  9355  ramub2  16985  ramub1lem2  16998  funcres  17858  gsumsplit1r  18614  gasubg  19234  gsumzaddlem  19851  dprdfadd  19952  dprdres  19960  dprdf1  19965  dmdprdsplitlem  19969  dmdprdsplit2lem  19977  dmdprdsplit2  19978  dprdsplit  19980  ablfac1eulem  20004  ablfac1eu  20005  pwssplit0  20965  frlmsplit2  21682  mamures  22284  mdetrlin  22489  cnrest  23172  cnpresti  23175  cnprest  23176  ptuncnv  23694  ptunhmeo  23695  ptcmpfi  23700  tsmslem1  24016  tsmssubm  24030  tsmsres  24031  tsmsf1o  24032  tsmsxplem1  24040  tsmsxplem2  24041  psmetres2  24202  xmetres2  24249  metres2  24251  imasdsf1olem  24261  xmetresbl  24325  xrge0gsumle  24722  xrge0tsms  24723  rescncf  24790  mbfres2  25546  limcres  25787  limciun  25795  dvres3  25814  dvmptresicc  25817  dvlip  25898  dvlipcn  25899  dvlip2  25900  dvgt0lem1  25907  dvivthlem1  25913  lhop  25921  ulmres  26297  ulmss  26306  pserdvlem2  26338  jensenlem2  26898  jensen  26899  wlkres  29598  pthdifv  29660  pthdlem1  29696  foresf1o  32433  resf1o  32653  pfxf1  32863  xrge0tsmsd  33002  gsumle  33038  tocyccntz  33101  elrspunsn  33400  rprmdvdsprod  33505  ply1degltdimlem  33618  zarcmplem  33871  measres  34212  omsmeas  34314  reprsuc  34606  f1resfz0f1d  35101  pfxwlk  35111  pthhashvtx  35115  cvmliftlem6  35277  cvmlift2lem11  35300  satfv1lem  35349  mrsubff1  35501  msubff1  35543  psrbagres  42534  evlselv  42575  fsuppssind  42581  aomclem4  43046  extoimad  44153  imo72b2lem0  44154  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  wessf1ornlem  45179  feqresmptf  45225  limcperiod  45626  climxlim2  45844  cncfperiod  45877  dirkercncflem4  46104  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem53  46157  fourierdlem74  46178  fourierdlem75  46179  fourierdlem81  46185  fourierdlem85  46189  fourierdlem88  46192  fourierdlem93  46197  fourierdlem94  46198  fourierdlem95  46199  fourierdlem100  46204  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  sge0tsms  46378  sge0sup  46389  sge0gerp  46393  sge0pnffigt  46394  sge0lefi  46396  sge0ltfirp  46398  sge0resplit  46404  sge0le  46405  sge0split  46407  sge0iun  46417  meadjun  46460  ismeannd  46465  psmeasurelem  46468  omeunle  46514  omeiunle  46515  caratheodory  46526  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  smflimsuplem3  46820  fcoresf1  47070  fcoresfo  47072  lincdifsn  48413