Theorem fvresd 6776

Description: The value of a restricted function, deduction version of fvres 6775. (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 6775	. 2 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ↾ cres 5582  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-res 5592  df-iota 6376  df-fv 6426

This theorem is referenced by:  fvressn  7016  fvsnun1  7036  fvsnun2  7037  fsnunfv  7041  resfvresima  7093  ovres  7416  curry1  7915  curry2  7918  frrlem4  8076  frrlem12  8084  smores  8154  smores2  8156  tz7.44-2  8209  seqomlem1  8251  seqomlem4  8254  onasuc  8320  onmsuc  8321  onesuc  8322  ordtypelem4  9210  ordtypelem6  9212  ordtypelem7  9213  unxpwdom2  9277  cantnfres  9365  cantnfp1lem3  9368  dfac12lem1  9830  ackbij2lem2  9927  cfsmolem  9957  ttukeylem3  10198  fpwwe2lem5  10322  fpwwe2lem8  10325  canthp1lem2  10340  addpqnq  10625  mulpqnq  10628  seqf1olem2  13691  seqcoll  14106  rlimres  15195  lo1res  15196  isercolllem3  15306  ackbijnn  15468  bitsf1  16081  sadcaddlem  16092  sadaddlem  16101  sadasslem  16105  sadeq  16107  eucalgcvga  16219  eucalg  16220  funcres  17527  1stf1  17825  2ndf1  17828  1stfcl  17830  2ndfcl  17831  prf1st  17837  prf2nd  17838  1st2ndprf  17839  uncf2  17871  diag12  17878  diag2  17879  curf2ndf  17881  yonedalem22  17912  lubval  17989  glbval  18002  gsumsplit1r  18286  resmhm  18374  resghm  18765  efgsres  19259  efgredlemd  19265  efgredlem  19268  dprdres  19546  dmdprdsplit2lem  19563  abvres  20014  reslmhm  20229  psgndiflemB  20717  cnpresti  22347  cnprest  22348  upxp  22682  uptx  22684  txkgen  22711  remetdval  23858  lmcau  24382  dvreslem  24978  dvres2lem  24979  dvlip2  25064  c1liplem1  25065  dvgt0lem1  25071  lhop1lem  25082  dvcnvrelem1  25086  dvcvx  25089  psercn  25490  efcvx  25513  reefgim  25514  resinf1o  25597  efif1olem4  25606  eff1olem  25609  eflog  25637  logcn  25707  loglesqrt  25816  asinrebnd  25956  jensen  26043  amgmlem  26044  lgamgulmlem2  26084  dvdsmulf1o  26248  dchrabs  26313  sum2dchr  26327  uhgrspansubgrlem  27560  wlkres  27940  redwlk  27942  ofresid  30880  2ndresdju  30887  fdifsuppconst  30925  ressupprn  30926  fsuppcurry1  30962  fsuppcurry2  30963  mgcf1o  31183  gsumpart  31217  gsumhashmul  31218  tocyccntz  31313  dimkerim  31610  zarcmplem  31733  measres  32090  ftc2re  32478  reprsuc  32495  bnj1379  32710  pfxwlk  32985  subgrwlk  32994  satom  33218  ttrclss  33706  nolesgn2o  33801  nolesgn2ores  33802  nogesgn1o  33803  nogesgn1ores  33804  noresle  33827  nosupprefixmo  33830  noinfprefixmo  33831  nosupres  33837  nosupbnd2lem1  33845  noinfres  33852  noinfbnd2lem1  33860  noetasuplem4  33866  noetainflem4  33870  addsval  34053  bj-fvsnun1  35353  fnwe2lem3  40793  wessf1ornlem  42611  limcperiod  43059  limclner  43082  limsupresxr  43197  liminfresxr  43198  cncfperiod  43310  sssmf  44161  fcores  44448  rhmsubclem2  45533  rhmsubcALTVlem2  45551