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

Theorem fssresd 6109
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 6108 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
41, 2, 3syl2anc 694 1 (𝜑 → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3607  cres 5145  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-fun 5928  df-fn 5929  df-f 5930
This theorem is referenced by:  feqresmpt  6289  fsuppcor  8350  ramub2  15765  ramub1lem2  15778  funcres  16603  gasubg  17781  gsumzaddlem  18367  dprdfadd  18465  dprdres  18473  dprdf1  18478  dmdprdsplitlem  18482  dmdprdsplit2lem  18490  dmdprdsplit2  18491  dprdsplit  18493  ablfac1eulem  18517  ablfac1eu  18518  pwssplit0  19106  frlmsplit2  20160  mamures  20244  mdetrlin  20456  cnrest  21137  cnpresti  21140  cnprest  21141  ptuncnv  21658  ptunhmeo  21659  ptcmpfi  21664  tsmslem1  21979  tsmssubm  21993  tsmsres  21994  tsmsf1o  21995  tsmsxplem1  22003  tsmsxplem2  22004  psmetres2  22166  xmetres2  22213  metres2  22215  imasdsf1olem  22225  xmetresbl  22289  xrge0gsumle  22683  xrge0tsms  22684  rescncf  22747  mbfres2  23457  limcres  23695  limciun  23703  dvres3  23722  dvlip  23801  dvlipcn  23802  dvlip2  23803  dvgt0lem1  23810  dvivthlem1  23816  lhop  23824  ulmres  24187  ulmss  24196  pserdvlem2  24227  jensenlem2  24759  jensen  24760  wlkres  26623  pthdlem1  26718  foresf1o  29469  resf1o  29633  gsumle  29907  xrge0tsmsd  29913  measres  30413  omsmeas  30513  reprsuc  30821  cvmliftlem6  31398  cvmlift2lem11  31421  mrsubff1  31537  msubff1  31579  aomclem4  37944  extoimad  38781  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  wessf1ornlem  39685  feqresmptf  39747  limcperiod  40178  climxlim2  40390  cncfperiod  40410  dvmptresicc  40452  dirkercncflem4  40641  fourierdlem48  40689  fourierdlem49  40690  fourierdlem51  40692  fourierdlem53  40694  fourierdlem74  40715  fourierdlem75  40716  fourierdlem81  40722  fourierdlem85  40726  fourierdlem88  40729  fourierdlem93  40734  fourierdlem94  40735  fourierdlem95  40736  fourierdlem100  40741  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  sge0tsms  40915  sge0sup  40926  sge0gerp  40930  sge0pnffigt  40931  sge0lefi  40933  sge0ltfirp  40935  sge0resplit  40941  sge0le  40942  sge0split  40944  sge0iun  40954  meadjun  40997  ismeannd  41002  psmeasurelem  41005  omeunle  41051  omeiunle  41052  caratheodory  41063  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  smflimsuplem3  41349  lincdifsn  42538
  Copyright terms: Public domain W3C validator