Theorem fssresd 6071

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	|- ( ph -> F : A --> B )
fssresd.2	|- ( ph -> C C_ A )

Assertion

Ref	Expression
fssresd	|- ( ph -> ( F |` C ) : C --> B )

Proof of Theorem fssresd

Step	Hyp	Ref	Expression
1		fssresd.1	. 2 |- ( ph -> F : A --> B )
2		fssresd.2	. 2 |- ( ph -> C C_ A )
3		fssres 6070	. 2 |- ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( F |` C ) : C --> B )

Syntax hints:   -> wi 4   C_ wss 3574   |` cres 5116   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-fun 5890  df-fn 5891  df-f 5892

This theorem is referenced by:  feqresmpt  6250  fsuppcor  8309  ramub2  15718  ramub1lem2  15731  funcres  16556  gasubg  17735  gsumzaddlem  18321  dprdfadd  18419  dprdres  18427  dprdf1  18432  dmdprdsplitlem  18436  dmdprdsplit2lem  18444  dmdprdsplit2  18445  dprdsplit  18447  ablfac1eulem  18471  ablfac1eu  18472  pwssplit0  19058  frlmsplit2  20112  mamures  20196  mdetrlin  20408  cnrest  21089  cnpresti  21092  cnprest  21093  ptuncnv  21610  ptunhmeo  21611  ptcmpfi  21616  tsmslem1  21932  tsmssubm  21946  tsmsres  21947  tsmsf1o  21948  tsmsxplem1  21956  tsmsxplem2  21957  psmetres2  22119  xmetres2  22166  metres2  22168  imasdsf1olem  22178  xmetresbl  22242  xrge0gsumle  22636  xrge0tsms  22637  rescncf  22700  mbfres2  23412  limcres  23650  limciun  23658  dvres3  23677  dvlip  23756  dvlipcn  23757  dvlip2  23758  dvgt0lem1  23765  dvivthlem1  23771  lhop  23779  ulmres  24142  ulmss  24151  pserdvlem2  24182  jensenlem2  24714  jensen  24715  wlkres  26567  pthdlem1  26662  foresf1o  29343  resf1o  29505  gsumle  29779  xrge0tsmsd  29785  measres  30285  omsmeas  30385  reprsuc  30693  cvmliftlem6  31272  cvmlift2lem11  31295  mrsubff1  31411  msubff1  31453  aomclem4  37627  extoimad  38464  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  wessf1ornlem  39371  feqresmptf  39433  limcperiod  39860  climxlim2  40072  cncfperiod  40092  dvmptresicc  40134  dirkercncflem4  40323  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem53  40376  fourierdlem74  40397  fourierdlem75  40398  fourierdlem81  40404  fourierdlem85  40408  fourierdlem88  40411  fourierdlem93  40416  fourierdlem94  40417  fourierdlem95  40418  fourierdlem100  40423  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  sge0tsms  40597  sge0sup  40608  sge0gerp  40612  sge0pnffigt  40613  sge0lefi  40615  sge0ltfirp  40617  sge0resplit  40623  sge0le  40624  sge0split  40626  sge0iun  40636  meadjun  40679  ismeannd  40684  psmeasurelem  40687  omeunle  40730  omeiunle  40731  caratheodory  40742  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  smflimsuplem3  41028  lincdifsn  42213