Theorem fvresd 6908

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ↾ cres 5677  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-xp 5681  df-res 5687  df-iota 6492  df-fv 6548

This theorem is referenced by:  fvressn  7156  fvsnun1  7176  fvsnun2  7177  fsnunfv  7181  resfvresima  7233  ovres  7569  curry1  8086  curry2  8089  frrlem4  8270  frrlem12  8278  smores  8348  smores2  8350  tz7.44-2  8403  seqomlem1  8446  seqomlem4  8449  onasuc  8524  onmsuc  8525  onesuc  8526  ordtypelem4  9512  ordtypelem6  9514  ordtypelem7  9515  unxpwdom2  9579  cantnfres  9668  cantnfp1lem3  9671  ttrclss  9711  dfac12lem1  10134  ackbij2lem2  10231  cfsmolem  10261  ttukeylem3  10502  fpwwe2lem5  10626  fpwwe2lem8  10629  canthp1lem2  10644  addpqnq  10929  mulpqnq  10932  seqf1olem2  14004  seqcoll  14421  rlimres  15498  lo1res  15499  isercolllem3  15609  ackbijnn  15770  bitsf1  16383  sadcaddlem  16394  sadaddlem  16403  sadasslem  16407  sadeq  16409  eucalgcvga  16519  eucalg  16520  funcres  17842  1stf1  18140  2ndf1  18143  1stfcl  18145  2ndfcl  18146  prf1st  18152  prf2nd  18153  1st2ndprf  18154  uncf2  18186  diag12  18193  diag2  18194  curf2ndf  18196  yonedalem22  18227  lubval  18305  glbval  18318  gsumsplit1r  18602  resmhm  18697  resghm  19102  efgsres  19600  efgredlemd  19606  efgredlem  19609  dprdres  19892  dmdprdsplit2lem  19909  imadrhmcl  20405  abvres  20439  reslmhm  20655  psgndiflemB  21144  cnpresti  22783  cnprest  22784  upxp  23118  uptx  23120  txkgen  23147  remetdval  24296  lmcau  24821  dvreslem  25417  dvres2lem  25418  dvlip2  25503  c1liplem1  25504  dvgt0lem1  25510  lhop1lem  25521  dvcnvrelem1  25525  dvcvx  25528  psercn  25929  efcvx  25952  reefgim  25953  resinf1o  26036  efif1olem4  26045  eff1olem  26048  eflog  26076  logcn  26146  loglesqrt  26255  asinrebnd  26395  jensen  26482  amgmlem  26483  lgamgulmlem2  26523  dvdsmulf1o  26687  dchrabs  26752  sum2dchr  26766  nolesgn2o  27163  nolesgn2ores  27164  nogesgn1o  27165  nogesgn1ores  27166  noresle  27189  nosupprefixmo  27192  noinfprefixmo  27193  nosupres  27199  nosupbnd2lem1  27207  noinfres  27214  noinfbnd2lem1  27222  noetasuplem4  27228  noetainflem4  27232  addsval  27435  mulsval  27554  uhgrspansubgrlem  28536  wlkres  28916  redwlk  28918  ofresid  31854  2ndresdju  31861  fdifsuppconst  31898  ressupprn  31899  fsuppcurry1  31937  fsuppcurry2  31938  mgcf1o  32160  gsumpart  32194  gsumhashmul  32195  tocyccntz  32290  elrspunsn  32535  evls1addd  32636  evls1muld  32637  evls1vsca  32638  ressply10g  32644  ply1gsumz  32657  dimkerim  32700  irngss  32739  evls1fvcl  32746  evls1maprhm  32747  evls1maprnss  32749  zarcmplem  32849  measres  33208  ftc2re  33598  reprsuc  33615  bnj1379  33829  pfxwlk  34102  subgrwlk  34111  satom  34335  bj-fvsnun1  36124  selvvvval  41154  evlselv  41156  fnwe2lem3  41779  wessf1ornlem  43867  limcperiod  44330  limclner  44353  limsupresxr  44468  liminfresxr  44469  cncfperiod  44581  sssmf  45440  fcores  45763  rhmsubclem2  46938  rhmsubcALTVlem2  46956