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

Theorem fssresd 6518
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 6517 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
41, 2, 3syl2anc 587 1 (𝜑 → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3910  cres 5530  wf 6324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-br 5040  df-opab 5102  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-fun 6330  df-fn 6331  df-f 6332
This theorem is referenced by:  feqresmpt  6707  fsuppcor  8843  ramub2  16327  ramub1lem2  16340  funcres  17144  gsumsplit1r  17875  gasubg  18410  gsumzaddlem  19019  dprdfadd  19120  dprdres  19128  dprdf1  19133  dmdprdsplitlem  19137  dmdprdsplit2lem  19145  dmdprdsplit2  19146  dprdsplit  19148  ablfac1eulem  19172  ablfac1eu  19173  pwssplit0  19805  frlmsplit2  20892  mamures  20976  mdetrlin  21186  cnrest  21868  cnpresti  21871  cnprest  21872  ptuncnv  22390  ptunhmeo  22391  ptcmpfi  22396  tsmslem1  22712  tsmssubm  22726  tsmsres  22727  tsmsf1o  22728  tsmsxplem1  22736  tsmsxplem2  22737  psmetres2  22899  xmetres2  22946  metres2  22948  imasdsf1olem  22958  xmetresbl  23022  xrge0gsumle  23416  xrge0tsms  23417  rescncf  23480  mbfres2  24227  limcres  24467  limciun  24475  dvres3  24494  dvmptresicc  24497  dvlip  24574  dvlipcn  24575  dvlip2  24576  dvgt0lem1  24583  dvivthlem1  24589  lhop  24597  ulmres  24961  ulmss  24970  pserdvlem2  25001  jensenlem2  25551  jensen  25552  wlkres  27438  pthdlem1  27533  foresf1o  30250  resf1o  30452  pfxf1  30604  xrge0tsmsd  30699  gsumle  30732  tocyccntz  30793  measres  31488  omsmeas  31588  reprsuc  31893  f1resfz0f1d  32368  pfxwlk  32377  pthhashvtx  32381  cvmliftlem6  32544  cvmlift2lem11  32567  satfv1lem  32616  mrsubff1  32768  msubff1  32810  aomclem4  39798  extoimad  40652  imo72b2lem0  40653  imo72b2lem2  40655  imo72b2lem1  40658  imo72b2  40662  wessf1ornlem  41601  feqresmptf  41655  limcperiod  42063  climxlim2  42281  cncfperiod  42314  dirkercncflem4  42541  fourierdlem48  42589  fourierdlem49  42590  fourierdlem51  42592  fourierdlem53  42594  fourierdlem74  42615  fourierdlem75  42616  fourierdlem81  42622  fourierdlem85  42626  fourierdlem88  42629  fourierdlem93  42634  fourierdlem94  42635  fourierdlem95  42636  fourierdlem100  42641  fourierdlem103  42644  fourierdlem104  42645  fourierdlem107  42648  fourierdlem111  42652  fourierdlem112  42653  fourierdlem113  42654  sge0tsms  42812  sge0sup  42823  sge0gerp  42827  sge0pnffigt  42828  sge0lefi  42830  sge0ltfirp  42832  sge0resplit  42838  sge0le  42839  sge0split  42841  sge0iun  42851  meadjun  42894  ismeannd  42899  psmeasurelem  42902  omeunle  42948  omeiunle  42949  caratheodory  42960  hoidmvlelem1  43027  hoidmvlelem2  43028  hoidmvlelem3  43029  hoidmvlelem4  43030  smflimsuplem3  43246  lincdifsn  44626
  Copyright terms: Public domain W3C validator