Theorem fvresd 6896

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ↾ cres 5656  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-res 5666  df-iota 6484  df-fv 6539

This theorem is referenced by:  fvressn  7152  fvsnun1  7174  fvsnun2  7175  fsnunfv  7179  resfvresima  7227  ovres  7573  resf1extb  7930  curry1  8103  curry2  8106  frrlem4  8288  frrlem12  8296  smores  8366  smores2  8368  tz7.44-2  8421  seqomlem1  8464  seqomlem4  8467  onasuc  8540  onmsuc  8541  onesuc  8542  ordtypelem4  9535  ordtypelem6  9537  ordtypelem7  9538  unxpwdom2  9602  cantnfres  9691  cantnfp1lem3  9694  ttrclss  9734  dfac12lem1  10158  ackbij2lem2  10253  cfsmolem  10284  ttukeylem3  10525  fpwwe2lem5  10649  fpwwe2lem8  10652  canthp1lem2  10667  addpqnq  10952  mulpqnq  10955  seqf1olem2  14060  seqcoll  14482  rlimres  15574  lo1res  15575  isercolllem3  15683  ackbijnn  15844  bitsf1  16465  sadcaddlem  16476  sadaddlem  16485  sadasslem  16489  sadeq  16491  eucalgcvga  16605  eucalg  16606  funcres  17909  1stf1  18204  2ndf1  18207  1stfcl  18209  2ndfcl  18210  prf1st  18216  prf2nd  18217  1st2ndprf  18218  uncf2  18249  diag12  18256  diag2  18257  curf2ndf  18259  yonedalem22  18290  lubval  18366  glbval  18379  gsumsplit1r  18665  resmhm  18798  resghm  19215  efgsres  19719  efgredlemd  19725  efgredlem  19728  dprdres  20011  dmdprdsplit2lem  20028  rhmsubclem2  20646  imadrhmcl  20757  abvres  20791  reslmhm  21010  psgndiflemB  21560  evls1addd  22309  evls1muld  22310  evls1vsca  22311  evls1fvcl  22313  evls1maprhm  22314  evls1maprnss  22316  cnpresti  23226  cnprest  23227  upxp  23561  uptx  23563  txkgen  23590  remetdval  24728  lmcau  25265  dvreslem  25862  dvres2lem  25863  dvlip2  25952  c1liplem1  25953  dvgt0lem1  25959  lhop1lem  25970  dvcnvrelem1  25974  dvcvx  25977  psercn  26388  efcvx  26411  reefgim  26412  resinf1o  26497  efif1olem4  26506  eff1olem  26509  eflog  26537  logcn  26608  loglesqrt  26723  asinrebnd  26863  jensen  26951  amgmlem  26952  lgamgulmlem2  26992  mpodvdsmulf1o  27156  dvdsmulf1o  27158  dchrabs  27223  sum2dchr  27237  nolesgn2o  27635  nolesgn2ores  27636  nogesgn1o  27637  nogesgn1ores  27638  noresle  27661  nosupprefixmo  27664  noinfprefixmo  27665  nosupres  27671  nosupbnd2lem1  27679  noinfres  27686  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  addsval  27921  mulsval  28064  onsiso  28221  uhgrspansubgrlem  29269  wlkres  29650  redwlk  29652  cyclnumvtx  29782  ofresid  32620  2ndresdju  32627  fdifsupp  32662  fdifsuppconst  32666  ressupprn  32667  fsuppcurry1  32702  fsuppcurry2  32703  mgcf1o  32983  gsumpart  33051  gsumhashmul  33055  tocyccntz  33155  elrspunsn  33444  ressply10g  33580  evls1subd  33585  ply1gsumz  33608  dimkerim  33667  irngss  33728  rtelextdg2lem  33760  zarcmplem  33912  measres  34253  ftc2re  34630  reprsuc  34647  bnj1379  34861  pfxwlk  35146  subgrwlk  35154  satom  35378  bj-fvsnun1  37273  selvvvval  42608  evlselv  42610  fnwe2lem3  43076  wessf1ornlem  45209  limcperiod  45657  limclner  45680  limsupresxr  45795  liminfresxr  45796  cncfperiod  45908  sssmf  46767  fcores  47096  isubgrgrim  47942  rhmsubcALTVlem2  48257  tposidres  48861  fuco11  49237