Theorem fssresd 6730

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

Syntax hints:   → wi 4   ⊆ wss 3917   ↾ cres 5643  ⟶wf 6510

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  feqresmpt  6933  resf1extb  7913  resf1ext2b  7914  fsuppcor  9362  ramub2  16992  ramub1lem2  17005  funcres  17865  gsumsplit1r  18621  gasubg  19241  gsumzaddlem  19858  dprdfadd  19959  dprdres  19967  dprdf1  19972  dmdprdsplitlem  19976  dmdprdsplit2lem  19984  dmdprdsplit2  19985  dprdsplit  19987  ablfac1eulem  20011  ablfac1eu  20012  pwssplit0  20972  frlmsplit2  21689  mamures  22291  mdetrlin  22496  cnrest  23179  cnpresti  23182  cnprest  23183  ptuncnv  23701  ptunhmeo  23702  ptcmpfi  23707  tsmslem1  24023  tsmssubm  24037  tsmsres  24038  tsmsf1o  24039  tsmsxplem1  24047  tsmsxplem2  24048  psmetres2  24209  xmetres2  24256  metres2  24258  imasdsf1olem  24268  xmetresbl  24332  xrge0gsumle  24729  xrge0tsms  24730  rescncf  24797  mbfres2  25553  limcres  25794  limciun  25802  dvres3  25821  dvmptresicc  25824  dvlip  25905  dvlipcn  25906  dvlip2  25907  dvgt0lem1  25914  dvivthlem1  25920  lhop  25928  ulmres  26304  ulmss  26313  pserdvlem2  26345  jensenlem2  26905  jensen  26906  wlkres  29605  pthdifv  29667  pthdlem1  29703  foresf1o  32440  resf1o  32660  pfxf1  32870  xrge0tsmsd  33009  gsumle  33045  tocyccntz  33108  elrspunsn  33407  rprmdvdsprod  33512  ply1degltdimlem  33625  zarcmplem  33878  measres  34219  omsmeas  34321  reprsuc  34613  f1resfz0f1d  35108  pfxwlk  35118  pthhashvtx  35122  cvmliftlem6  35284  cvmlift2lem11  35307  satfv1lem  35356  mrsubff1  35508  msubff1  35550  psrbagres  42541  evlselv  42582  fsuppssind  42588  aomclem4  43053  extoimad  44160  imo72b2lem0  44161  imo72b2lem2  44163  imo72b2lem1  44165  imo72b2  44168  wessf1ornlem  45186  feqresmptf  45232  limcperiod  45633  climxlim2  45851  cncfperiod  45884  dirkercncflem4  46111  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem53  46164  fourierdlem74  46185  fourierdlem75  46186  fourierdlem81  46192  fourierdlem85  46196  fourierdlem88  46199  fourierdlem93  46204  fourierdlem94  46205  fourierdlem95  46206  fourierdlem100  46211  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  sge0tsms  46385  sge0sup  46396  sge0gerp  46400  sge0pnffigt  46401  sge0lefi  46403  sge0ltfirp  46405  sge0resplit  46411  sge0le  46412  sge0split  46414  sge0iun  46424  meadjun  46467  ismeannd  46472  psmeasurelem  46475  omeunle  46521  omeiunle  46522  caratheodory  46533  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  smflimsuplem3  46827  fcoresf1  47074  fcoresfo  47076  lincdifsn  48417