Theorem fvresd 6940

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ↾ cres 5702  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-res 5712  df-iota 6525  df-fv 6581

This theorem is referenced by:  fvressn  7196  fvsnun1  7216  fvsnun2  7217  fsnunfv  7221  resfvresima  7272  ovres  7616  curry1  8145  curry2  8148  frrlem4  8330  frrlem12  8338  smores  8408  smores2  8410  tz7.44-2  8463  seqomlem1  8506  seqomlem4  8509  onasuc  8584  onmsuc  8585  onesuc  8586  ordtypelem4  9590  ordtypelem6  9592  ordtypelem7  9593  unxpwdom2  9657  cantnfres  9746  cantnfp1lem3  9749  ttrclss  9789  dfac12lem1  10213  ackbij2lem2  10308  cfsmolem  10339  ttukeylem3  10580  fpwwe2lem5  10704  fpwwe2lem8  10707  canthp1lem2  10722  addpqnq  11007  mulpqnq  11010  seqf1olem2  14093  seqcoll  14513  rlimres  15604  lo1res  15605  isercolllem3  15715  ackbijnn  15876  bitsf1  16492  sadcaddlem  16503  sadaddlem  16512  sadasslem  16516  sadeq  16518  eucalgcvga  16633  eucalg  16634  funcres  17960  1stf1  18261  2ndf1  18264  1stfcl  18266  2ndfcl  18267  prf1st  18273  prf2nd  18274  1st2ndprf  18275  uncf2  18307  diag12  18314  diag2  18315  curf2ndf  18317  yonedalem22  18348  lubval  18426  glbval  18439  gsumsplit1r  18725  resmhm  18855  resghm  19272  efgsres  19780  efgredlemd  19786  efgredlem  19789  dprdres  20072  dmdprdsplit2lem  20089  rhmsubclem2  20708  imadrhmcl  20820  abvres  20854  reslmhm  21074  psgndiflemB  21641  evls1addd  22396  evls1muld  22397  evls1vsca  22398  evls1fvcl  22400  evls1maprhm  22401  evls1maprnss  22403  cnpresti  23317  cnprest  23318  upxp  23652  uptx  23654  txkgen  23681  remetdval  24830  lmcau  25366  dvreslem  25964  dvres2lem  25965  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  lhop1lem  26072  dvcnvrelem1  26076  dvcvx  26079  psercn  26488  efcvx  26511  reefgim  26512  resinf1o  26596  efif1olem4  26605  eff1olem  26608  eflog  26636  logcn  26707  loglesqrt  26822  asinrebnd  26962  jensen  27050  amgmlem  27051  lgamgulmlem2  27091  mpodvdsmulf1o  27255  dvdsmulf1o  27257  dchrabs  27322  sum2dchr  27336  nolesgn2o  27734  nolesgn2ores  27735  nogesgn1o  27736  nogesgn1ores  27737  noresle  27760  nosupprefixmo  27763  noinfprefixmo  27764  nosupres  27770  nosupbnd2lem1  27778  noinfres  27785  noinfbnd2lem1  27793  noetasuplem4  27799  noetainflem4  27803  addsval  28013  mulsval  28153  uhgrspansubgrlem  29325  wlkres  29706  redwlk  29708  ofresid  32661  2ndresdju  32667  fdifsuppconst  32701  ressupprn  32702  fsuppcurry1  32739  fsuppcurry2  32740  mgcf1o  32976  gsumpart  33038  gsumhashmul  33040  tocyccntz  33137  elrspunsn  33422  ressply10g  33557  evls1subd  33562  ply1gsumz  33584  dimkerim  33640  irngss  33687  rtelextdg2lem  33717  zarcmplem  33827  measres  34186  ftc2re  34575  reprsuc  34592  bnj1379  34806  pfxwlk  35091  subgrwlk  35100  satom  35324  bj-fvsnun1  37221  selvvvval  42540  evlselv  42542  fnwe2lem3  43009  wessf1ornlem  45092  limcperiod  45549  limclner  45572  limsupresxr  45687  liminfresxr  45688  cncfperiod  45800  sssmf  46659  fcores  46982  isubgrgrim  47781  rhmsubcALTVlem2  48005