MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fssresd Structured version   Visualization version   GIF version

Theorem fssresd 6710
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
StepHypRef Expression
1 fssresd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 fssresd.2 . 2 (𝜑𝐶𝐴)
3 fssres 6709 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
41, 2, 3syl2anc 585 1 (𝜑 → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3911  cres 5636  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  feqresmpt  6912  fsuppcor  9341  ramub2  16887  ramub1lem2  16900  funcres  17783  gsumsplit1r  18543  gasubg  19083  gsumzaddlem  19699  dprdfadd  19800  dprdres  19808  dprdf1  19813  dmdprdsplitlem  19817  dmdprdsplit2lem  19825  dmdprdsplit2  19826  dprdsplit  19828  ablfac1eulem  19852  ablfac1eu  19853  pwssplit0  20522  frlmsplit2  21182  mamures  21742  mdetrlin  21954  cnrest  22639  cnpresti  22642  cnprest  22643  ptuncnv  23161  ptunhmeo  23162  ptcmpfi  23167  tsmslem1  23483  tsmssubm  23497  tsmsres  23498  tsmsf1o  23499  tsmsxplem1  23507  tsmsxplem2  23508  psmetres2  23670  xmetres2  23717  metres2  23719  imasdsf1olem  23729  xmetresbl  23793  xrge0gsumle  24199  xrge0tsms  24200  rescncf  24263  mbfres2  25012  limcres  25253  limciun  25261  dvres3  25280  dvmptresicc  25283  dvlip  25360  dvlipcn  25361  dvlip2  25362  dvgt0lem1  25369  dvivthlem1  25375  lhop  25383  ulmres  25750  ulmss  25759  pserdvlem2  25790  jensenlem2  26340  jensen  26341  wlkres  28621  pthdlem1  28717  foresf1o  31434  resf1o  31650  pfxf1  31801  xrge0tsmsd  31902  gsumle  31935  tocyccntz  31996  zarcmplem  32465  measres  32824  omsmeas  32926  reprsuc  33231  f1resfz0f1d  33707  pfxwlk  33720  pthhashvtx  33724  cvmliftlem6  33887  cvmlift2lem11  33910  satfv1lem  33959  mrsubff1  34111  msubff1  34153  fsuppssind  40771  aomclem4  41387  extoimad  42444  imo72b2lem0  42445  imo72b2lem2  42447  imo72b2lem1  42449  imo72b2  42452  wessf1ornlem  43410  feqresmptf  43461  limcperiod  43876  climxlim2  44094  cncfperiod  44127  dirkercncflem4  44354  fourierdlem48  44402  fourierdlem49  44403  fourierdlem51  44405  fourierdlem53  44407  fourierdlem74  44428  fourierdlem75  44429  fourierdlem81  44435  fourierdlem85  44439  fourierdlem88  44442  fourierdlem93  44447  fourierdlem94  44448  fourierdlem95  44449  fourierdlem100  44454  fourierdlem103  44457  fourierdlem104  44458  fourierdlem107  44461  fourierdlem111  44465  fourierdlem112  44466  fourierdlem113  44467  sge0tsms  44628  sge0sup  44639  sge0gerp  44643  sge0pnffigt  44644  sge0lefi  44646  sge0ltfirp  44648  sge0resplit  44654  sge0le  44655  sge0split  44657  sge0iun  44667  meadjun  44710  ismeannd  44715  psmeasurelem  44718  omeunle  44764  omeiunle  44765  caratheodory  44776  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem4  44846  smflimsuplem3  45070  fcoresf1  45310  fcoresfo  45312  lincdifsn  46512
  Copyright terms: Public domain W3C validator