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

Theorem fssresd 5969
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 5968 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
41, 2, 3syl2anc 691 1 (𝜑 → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3540  cres 5030  wf 5786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579  df-opab 4639  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-fun 5792  df-fn 5793  df-f 5794
This theorem is referenced by:  feqresmpt  6145  fsuppcor  8170  ramub2  15505  ramub1lem2  15518  funcres  16328  gasubg  17507  gsumzaddlem  18093  dprdfadd  18191  dprdres  18199  dprdf1  18204  dmdprdsplitlem  18208  dmdprdsplit2lem  18216  dmdprdsplit2  18217  dprdsplit  18219  ablfac1eulem  18243  ablfac1eu  18244  pwssplit0  18828  frlmsplit2  19879  mamures  19963  mdetrlin  20175  cnrest  20847  cnpresti  20850  cnprest  20851  ptuncnv  21368  ptunhmeo  21369  ptcmpfi  21374  tsmslem1  21690  tsmssubm  21704  tsmsres  21705  tsmsf1o  21706  tsmsxplem1  21714  tsmsxplem2  21715  psmetres2  21877  xmetres2  21924  metres2  21926  imasdsf1olem  21936  xmetresbl  22000  xrge0gsumle  22392  xrge0tsms  22393  rescncf  22456  mbfres2  23163  limcres  23401  limciun  23409  dvres3  23428  dvlip  23505  dvlipcn  23506  dvlip2  23507  dvgt0lem1  23514  dvivthlem1  23520  lhop  23528  ulmres  23891  ulmss  23900  pserdvlem2  23931  jensenlem2  24459  jensen  24460  uhgrares  25631  umgrares  25647  eupares  26296  foresf1o  28521  resf1o  28687  gsumle  28904  xrge0tsmsd  28910  measres  29406  omsmeas  29506  cvmliftlem6  30320  cvmlift2lem11  30343  mrsubff1  30459  msubff1  30501  aomclem4  36439  extoimad  37280  imo72b2lem0  37281  imo72b2lem2  37283  imo72b2lem1  37287  imo72b2  37291  wessf1ornlem  38160  limcperiod  38489  cncfperiod  38558  dvmptresicc  38603  dirkercncflem4  38793  fourierdlem48  38841  fourierdlem49  38842  fourierdlem51  38844  fourierdlem53  38846  fourierdlem74  38867  fourierdlem75  38868  fourierdlem81  38874  fourierdlem85  38878  fourierdlem88  38881  fourierdlem93  38886  fourierdlem94  38887  fourierdlem95  38888  fourierdlem100  38893  fourierdlem103  38896  fourierdlem104  38897  fourierdlem107  38900  fourierdlem111  38904  fourierdlem112  38905  fourierdlem113  38906  sge0tsms  39067  sge0sup  39078  sge0gerp  39082  sge0pnffigt  39083  sge0lefi  39085  sge0ltfirp  39087  sge0resplit  39093  sge0le  39094  sge0split  39096  sge0iun  39106  meadjun  39149  ismeannd  39154  psmeasurelem  39157  omeunle  39200  omeiunle  39201  caratheodory  39212  hoidmvlelem1  39279  hoidmvlelem2  39280  hoidmvlelem3  39281  hoidmvlelem4  39282  1wlkres  40871  pthdlem1  40964  lincdifsn  41999
  Copyright terms: Public domain W3C validator