Theorem fvresd 6912

Description: The value of a restricted function, deduction version of fvres 6911. (Contributed by Glauco Siliprandi, 8-Apr-2021.)

Hypothesis

Ref	Expression
fvresd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)

Assertion

Ref	Expression
fvresd	⊢ (𝜑 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Proof of Theorem fvresd

Step	Hyp	Ref	Expression
1		fvresd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		fvres 6911	. 2 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ↾ cres 5679  ‘cfv 6544

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

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 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-xp 5683  df-res 5689  df-iota 6496  df-fv 6552

This theorem is referenced by:  fvressn  7160  fvsnun1  7180  fvsnun2  7181  fsnunfv  7185  resfvresima  7237  ovres  7573  curry1  8090  curry2  8093  frrlem4  8274  frrlem12  8282  smores  8352  smores2  8354  tz7.44-2  8407  seqomlem1  8450  seqomlem4  8453  onasuc  8528  onmsuc  8529  onesuc  8530  ordtypelem4  9516  ordtypelem6  9518  ordtypelem7  9519  unxpwdom2  9583  cantnfres  9672  cantnfp1lem3  9675  ttrclss  9715  dfac12lem1  10138  ackbij2lem2  10235  cfsmolem  10265  ttukeylem3  10506  fpwwe2lem5  10630  fpwwe2lem8  10633  canthp1lem2  10648  addpqnq  10933  mulpqnq  10936  seqf1olem2  14008  seqcoll  14425  rlimres  15502  lo1res  15503  isercolllem3  15613  ackbijnn  15774  bitsf1  16387  sadcaddlem  16398  sadaddlem  16407  sadasslem  16411  sadeq  16413  eucalgcvga  16523  eucalg  16524  funcres  17846  1stf1  18144  2ndf1  18147  1stfcl  18149  2ndfcl  18150  prf1st  18156  prf2nd  18157  1st2ndprf  18158  uncf2  18190  diag12  18197  diag2  18198  curf2ndf  18200  yonedalem22  18231  lubval  18309  glbval  18322  gsumsplit1r  18606  resmhm  18701  resghm  19108  efgsres  19606  efgredlemd  19612  efgredlem  19615  dprdres  19898  dmdprdsplit2lem  19915  imadrhmcl  20413  abvres  20447  reslmhm  20663  psgndiflemB  21153  cnpresti  22792  cnprest  22793  upxp  23127  uptx  23129  txkgen  23156  remetdval  24305  lmcau  24830  dvreslem  25426  dvres2lem  25427  dvlip2  25512  c1liplem1  25513  dvgt0lem1  25519  lhop1lem  25530  dvcnvrelem1  25534  dvcvx  25537  psercn  25938  efcvx  25961  reefgim  25962  resinf1o  26045  efif1olem4  26054  eff1olem  26057  eflog  26085  logcn  26155  loglesqrt  26266  asinrebnd  26406  jensen  26493  amgmlem  26494  lgamgulmlem2  26534  dvdsmulf1o  26698  dchrabs  26763  sum2dchr  26777  nolesgn2o  27174  nolesgn2ores  27175  nogesgn1o  27176  nogesgn1ores  27177  noresle  27200  nosupprefixmo  27203  noinfprefixmo  27204  nosupres  27210  nosupbnd2lem1  27218  noinfres  27225  noinfbnd2lem1  27233  noetasuplem4  27239  noetainflem4  27243  addsval  27446  mulsval  27565  uhgrspansubgrlem  28547  wlkres  28927  redwlk  28929  ofresid  31867  2ndresdju  31874  fdifsuppconst  31911  ressupprn  31912  fsuppcurry1  31950  fsuppcurry2  31951  mgcf1o  32173  gsumpart  32207  gsumhashmul  32208  tocyccntz  32303  elrspunsn  32547  evls1addd  32648  evls1muld  32649  evls1vsca  32650  ressply10g  32656  ply1gsumz  32669  dimkerim  32712  irngss  32751  evls1fvcl  32758  evls1maprhm  32759  evls1maprnss  32761  zarcmplem  32861  measres  33220  ftc2re  33610  reprsuc  33627  bnj1379  33841  pfxwlk  34114  subgrwlk  34123  satom  34347  bj-fvsnun1  36136  selvvvval  41157  evlselv  41159  fnwe2lem3  41794  wessf1ornlem  43882  limcperiod  44344  limclner  44367  limsupresxr  44482  liminfresxr  44483  cncfperiod  44595  sssmf  45454  fcores  45777  rhmsubclem2  46985  rhmsubcALTVlem2  47003