Theorem fvresd 6926

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ↾ cres 5690  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-res 5700  df-iota 6515  df-fv 6570

This theorem is referenced by:  fvressn  7181  fvsnun1  7201  fvsnun2  7202  fsnunfv  7206  resfvresima  7254  ovres  7598  curry1  8127  curry2  8130  frrlem4  8312  frrlem12  8320  smores  8390  smores2  8392  tz7.44-2  8445  seqomlem1  8488  seqomlem4  8491  onasuc  8564  onmsuc  8565  onesuc  8566  ordtypelem4  9558  ordtypelem6  9560  ordtypelem7  9561  unxpwdom2  9625  cantnfres  9714  cantnfp1lem3  9717  ttrclss  9757  dfac12lem1  10181  ackbij2lem2  10276  cfsmolem  10307  ttukeylem3  10548  fpwwe2lem5  10672  fpwwe2lem8  10675  canthp1lem2  10690  addpqnq  10975  mulpqnq  10978  seqf1olem2  14079  seqcoll  14499  rlimres  15590  lo1res  15591  isercolllem3  15699  ackbijnn  15860  bitsf1  16479  sadcaddlem  16490  sadaddlem  16499  sadasslem  16503  sadeq  16505  eucalgcvga  16619  eucalg  16620  funcres  17946  1stf1  18247  2ndf1  18250  1stfcl  18252  2ndfcl  18253  prf1st  18259  prf2nd  18260  1st2ndprf  18261  uncf2  18293  diag12  18300  diag2  18301  curf2ndf  18303  yonedalem22  18334  lubval  18413  glbval  18426  gsumsplit1r  18712  resmhm  18845  resghm  19262  efgsres  19770  efgredlemd  19776  efgredlem  19779  dprdres  20062  dmdprdsplit2lem  20079  rhmsubclem2  20702  imadrhmcl  20814  abvres  20848  reslmhm  21068  psgndiflemB  21635  evls1addd  22390  evls1muld  22391  evls1vsca  22392  evls1fvcl  22394  evls1maprhm  22395  evls1maprnss  22397  cnpresti  23311  cnprest  23312  upxp  23646  uptx  23648  txkgen  23675  remetdval  24824  lmcau  25360  dvreslem  25958  dvres2lem  25959  dvlip2  26048  c1liplem1  26049  dvgt0lem1  26055  lhop1lem  26066  dvcnvrelem1  26070  dvcvx  26073  psercn  26484  efcvx  26507  reefgim  26508  resinf1o  26592  efif1olem4  26601  eff1olem  26604  eflog  26632  logcn  26703  loglesqrt  26818  asinrebnd  26958  jensen  27046  amgmlem  27047  lgamgulmlem2  27087  mpodvdsmulf1o  27251  dvdsmulf1o  27253  dchrabs  27318  sum2dchr  27332  nolesgn2o  27730  nolesgn2ores  27731  nogesgn1o  27732  nogesgn1ores  27733  noresle  27756  nosupprefixmo  27759  noinfprefixmo  27760  nosupres  27766  nosupbnd2lem1  27774  noinfres  27781  noinfbnd2lem1  27789  noetasuplem4  27795  noetainflem4  27799  addsval  28009  mulsval  28149  uhgrspansubgrlem  29321  wlkres  29702  redwlk  29704  ofresid  32658  2ndresdju  32665  fdifsupp  32699  fdifsuppconst  32703  ressupprn  32704  fsuppcurry1  32742  fsuppcurry2  32743  mgcf1o  32977  gsumpart  33042  gsumhashmul  33046  tocyccntz  33146  elrspunsn  33436  ressply10g  33571  evls1subd  33576  ply1gsumz  33598  dimkerim  33654  irngss  33701  rtelextdg2lem  33731  zarcmplem  33841  measres  34202  ftc2re  34591  reprsuc  34608  bnj1379  34822  pfxwlk  35107  subgrwlk  35116  satom  35340  bj-fvsnun1  37237  selvvvval  42571  evlselv  42573  fnwe2lem3  43040  wessf1ornlem  45127  limcperiod  45583  limclner  45606  limsupresxr  45721  liminfresxr  45722  cncfperiod  45834  sssmf  46693  fcores  47016  isubgrgrim  47834  rhmsubcALTVlem2  48125