Theorem fssresd 5777

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

Syntax hints:   -> wi 4   C_ wss 3416   |` cres 4858   -->wf 5601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419  df-opab 4478  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-fun 5607  df-fn 5608  df-f 5609

This theorem is referenced by:  feqresmpt  5946  fsuppcor  7948  ramub2  15026  ramub1lem2  15040  funcres  15856  gasubg  17011  gsumzaddlem  17609  dprdfadd  17708  dprdres  17716  dprdf1  17721  dmdprdsplitlem  17725  dmdprdsplit2lem  17733  dmdprdsplit2  17734  dprdsplit  17736  ablfac1eulem  17760  ablfac1eu  17761  pwssplit0  18336  frlmsplit2  19386  mamures  19470  mdetrlin  19682  cnrest  20356  cnpresti  20359  cnprest  20360  ptuncnv  20877  ptunhmeo  20878  ptcmpfi  20883  tsmslem1  21198  tsmssubm  21212  tsmsres  21213  tsmsf1o  21214  tsmsxplem1  21222  tsmsxplem2  21223  psmetres2  21385  xmetres2  21431  metres2  21433  imasdsf1olem  21443  xmetresbl  21507  xrge0gsumle  21906  xrge0tsms  21907  rescncf  21984  mbfres2  22657  limcres  22897  limciun  22905  dvres3  22924  dvlip  23001  dvlipcn  23002  dvlip2  23003  dvgt0lem1  23010  dvivthlem1  23016  lhop  23024  ulmres  23399  ulmss  23408  pserdvlem2  23439  jensenlem2  23969  jensen  23970  uhgrares  25091  umgrares  25107  eupares  25759  foresf1o  28195  resf1o  28367  gsumle  28593  xrge0tsmsd  28599  measres  29095  omsmeas  29205  omsmeasOLD  29206  cvmliftlem6  30063  cvmlift2lem11  30086  mrsubff1  30202  msubff1  30244  aomclem4  35961  extoimad  36653  imo72b2lem0  36654  imo72b2lem2  36656  imo72b2lem1  36660  imo72b2  36664  wessf1ornlem  37513  limcperiod  37794  cncfperiod  37842  dvmptresicc  37877  dirkercncflem4  38069  fourierdlem48  38119  fourierdlem49  38120  fourierdlem51  38122  fourierdlem53  38124  fourierdlem74  38145  fourierdlem75  38146  fourierdlem81  38152  fourierdlem85  38156  fourierdlem88  38159  fourierdlem93  38164  fourierdlem94  38165  fourierdlem95  38166  fourierdlem100  38171  fourierdlem103  38174  fourierdlem104  38175  fourierdlem107  38178  fourierdlem111  38182  fourierdlem112  38183  fourierdlem113  38184  sge0tsms  38325  sge0sup  38336  sge0gerp  38340  sge0pnffigt  38341  sge0lefi  38343  sge0ltfirp  38345  sge0resplit  38351  sge0le  38352  sge0split  38354  sge0iun  38364  meadjun  38405  ismeannd  38410  psmeasurelem  38413  omeunle  38445  omeiunle  38446  caratheodory  38457  hoidmvlelem1  38524  hoidmvlelem2  38525  hoidmvlelem3  38526  hoidmvlelem4  38527  pthdlem1  39888  uhgres  40060  lincdifsn  40586