Theorem fssresd 5767

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 5766	. 2 |- ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )
4	1, 2, 3	syl2anc 665	1 |- ( ph -> ( F |` C ) : C --> B )

Syntax hints:   -> wi 4   C_ wss 3436   |` cres 4855   -->wf 5597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-fun 5603  df-fn 5604  df-f 5605

This theorem is referenced by:  feqresmpt  5936  fsuppcor  7927  ramub2  14971  ramub1lem2  14985  funcres  15801  gasubg  16956  gsumzaddlem  17554  dprdfadd  17653  dprdres  17661  dprdf1  17666  dmdprdsplitlem  17670  dmdprdsplit2lem  17678  dmdprdsplit2  17679  dprdsplit  17681  ablfac1eulem  17705  ablfac1eu  17706  pwssplit0  18281  frlmsplit2  19330  mamures  19414  mdetrlin  19626  cnrest  20300  cnpresti  20303  cnprest  20304  ptuncnv  20821  ptunhmeo  20822  ptcmpfi  20827  tsmslem1  21142  tsmssubm  21156  tsmsres  21157  tsmsf1o  21158  tsmsxplem1  21166  tsmsxplem2  21167  psmetres2  21329  xmetres2  21375  metres2  21377  imasdsf1olem  21387  xmetresbl  21451  xrge0gsumle  21850  xrge0tsms  21851  rescncf  21928  mbfres2  22600  limcres  22840  limciun  22848  dvres3  22867  dvlip  22944  dvlipcn  22945  dvlip2  22946  dvgt0lem1  22953  dvivthlem1  22959  lhop  22967  ulmres  23342  ulmss  23351  pserdvlem2  23382  jensenlem2  23912  jensen  23913  uhgrares  25034  umgrares  25050  eupares  25702  foresf1o  28139  resf1o  28322  gsumle  28550  xrge0tsmsd  28557  measres  29053  omsmeas  29164  omsmeasOLD  29165  cvmliftlem6  30022  cvmlift2lem11  30045  mrsubff1  30161  msubff1  30203  aomclem4  35886  extoimad  36578  imo72b2lem0  36579  imo72b2lem2  36581  imo72b2lem1  36585  imo72b2  36590  wessf1ornlem  37421  limcperiod  37649  cncfperiod  37697  dvmptresicc  37732  dirkercncflem4  37909  fourierdlem48  37959  fourierdlem49  37960  fourierdlem51  37962  fourierdlem53  37964  fourierdlem74  37985  fourierdlem75  37986  fourierdlem81  37992  fourierdlem85  37996  fourierdlem88  37999  fourierdlem93  38004  fourierdlem94  38005  fourierdlem95  38006  fourierdlem100  38011  fourierdlem103  38014  fourierdlem104  38015  fourierdlem107  38018  fourierdlem111  38022  fourierdlem112  38023  fourierdlem113  38024  sge0tsms  38131  sge0sup  38142  sge0gerp  38146  sge0pnffigt  38147  sge0lefi  38149  sge0ltfirp  38151  sge0resplit  38157  sge0le  38158  sge0split  38160  sge0iun  38170  meadjun  38209  ismeannd  38214  psmeasurelem  38217  omeunle  38246  omeiunle  38247  caratheodory  38258  hoidmvlelem1  38322  hoidmvlelem2  38323  hoidmvlelem3  38324  hoidmvlelem4  38325  uhgres  39340  lincdifsn  39868