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 1542   ∈ wcel 2107   ↾ cres 5677  ‘cfv 6540

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 5298  ax-nul 5305  ax-pr 5426

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 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  7155  fvsnun1  7175  fvsnun2  7176  fsnunfv  7180  resfvresima  7232  ovres  7568  curry1  8085  curry2  8088  frrlem4  8269  frrlem12  8277  smores  8347  smores2  8349  tz7.44-2  8402  seqomlem1  8445  seqomlem4  8448  onasuc  8523  onmsuc  8524  onesuc  8525  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  19599  efgredlemd  19605  efgredlem  19608  dprdres  19890  dmdprdsplit2lem  19907  imadrhmcl  20401  abvres  20435  reslmhm  20651  psgndiflemB  21137  cnpresti  22774  cnprest  22775  upxp  23109  uptx  23111  txkgen  23138  remetdval  24287  lmcau  24812  dvreslem  25408  dvres2lem  25409  dvlip2  25494  c1liplem1  25495  dvgt0lem1  25501  lhop1lem  25512  dvcnvrelem1  25516  dvcvx  25519  psercn  25920  efcvx  25943  reefgim  25944  resinf1o  26027  efif1olem4  26036  eff1olem  26039  eflog  26067  logcn  26137  loglesqrt  26246  asinrebnd  26386  jensen  26473  amgmlem  26474  lgamgulmlem2  26514  dvdsmulf1o  26678  dchrabs  26743  sum2dchr  26757  nolesgn2o  27154  nolesgn2ores  27155  nogesgn1o  27156  nogesgn1ores  27157  noresle  27180  nosupprefixmo  27183  noinfprefixmo  27184  nosupres  27190  nosupbnd2lem1  27198  noinfres  27205  noinfbnd2lem1  27213  noetasuplem4  27219  noetainflem4  27223  addsval  27426  mulsval  27545  uhgrspansubgrlem  28527  wlkres  28907  redwlk  28909  ofresid  31845  2ndresdju  31852  fdifsuppconst  31889  ressupprn  31890  fsuppcurry1  31928  fsuppcurry2  31929  mgcf1o  32151  gsumpart  32185  gsumhashmul  32186  tocyccntz  32281  elrspunsn  32505  evls1addd  32598  evls1muld  32599  evls1vsca  32600  ressply10g  32603  ply1gsumz  32616  dimkerim  32657  irngss  32696  evls1maprhm  32703  evls1maprnss  32705  zarcmplem  32799  measres  33158  ftc2re  33548  reprsuc  33565  bnj1379  33779  pfxwlk  34052  subgrwlk  34061  satom  34285  bj-fvsnun1  36074  selvvvval  41107  evlselv  41109  fnwe2lem3  41727  wessf1ornlem  43815  limcperiod  44279  limclner  44302  limsupresxr  44417  liminfresxr  44418  cncfperiod  44530  sssmf  45389  fcores  45712  rhmsubclem2  46887  rhmsubcALTVlem2  46905