Theorem fvresd 6847

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ↾ cres 5620  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-res 5630  df-iota 6441  df-fv 6493

This theorem is referenced by:  fvressn  7105  fvsnun1  7126  fvsnun2  7127  fsnunfv  7131  resfvresima  7179  ovres  7522  resf1extb  7874  curry1  8043  curry2  8046  frrlem4  8229  frrlem12  8237  smores  8282  smores2  8284  tz7.44-2  8336  seqomlem1  8379  seqomlem4  8382  onasuc  8453  onmsuc  8454  onesuc  8455  ordtypelem4  9426  ordtypelem6  9428  ordtypelem7  9429  unxpwdom2  9493  cantnfres  9589  cantnfp1lem3  9592  ttrclss  9632  dfac12lem1  10057  ackbij2lem2  10152  cfsmolem  10183  ttukeylem3  10424  fpwwe2lem5  10549  fpwwe2lem8  10552  canthp1lem2  10567  addpqnq  10852  mulpqnq  10855  seqf1olem2  13995  seqcoll  14417  rlimres  15511  lo1res  15512  isercolllem3  15620  ackbijnn  15784  bitsf1  16406  sadcaddlem  16417  sadaddlem  16426  sadasslem  16430  sadeq  16432  eucalgcvga  16546  eucalg  16547  funcres  17854  1stf1  18149  2ndf1  18152  1stfcl  18154  2ndfcl  18155  prf1st  18161  prf2nd  18162  1st2ndprf  18163  uncf2  18194  diag12  18201  diag2  18202  curf2ndf  18204  yonedalem22  18235  lubval  18311  glbval  18324  gsumsplit1r  18646  resmhm  18779  resghm  19198  efgsres  19704  efgredlemd  19710  efgredlem  19713  dprdres  19996  dmdprdsplit2lem  20013  rhmsubclem2  20658  imadrhmcl  20769  abvres  20803  reslmhm  21042  psgndiflemB  21575  selvvvval  22118  evls1addd  22357  evls1muld  22358  evls1vsca  22359  evls1fvcl  22361  evls1maprhm  22362  evls1maprnss  22364  cnpresti  23271  cnprest  23272  upxp  23606  uptx  23608  txkgen  23635  remetdval  24772  lmcau  25298  dvreslem  25894  dvres2lem  25895  dvlip2  25980  c1liplem1  25981  dvgt0lem1  25987  lhop1lem  25998  dvcnvrelem1  26002  dvcvx  26005  psercn  26409  efcvx  26432  reefgim  26433  resinf1o  26518  efif1olem4  26527  eff1olem  26530  eflog  26558  logcn  26629  loglesqrt  26743  asinrebnd  26883  jensen  26970  amgmlem  26971  lgamgulmlem2  27011  mpodvdsmulf1o  27175  dvdsmulf1o  27177  dchrabs  27241  sum2dchr  27255  nolesgn2o  27653  nolesgn2ores  27654  nogesgn1o  27655  nogesgn1ores  27656  noresle  27679  nosupprefixmo  27682  noinfprefixmo  27683  nosupres  27689  nosupbnd2lem1  27697  noinfres  27704  noinfbnd2lem1  27712  noetasuplem4  27718  noetainflem4  27722  addsval  27972  mulsval  28119  oniso  28281  addonbday  28289  bdayfinlem  28496  uhgrspansubgrlem  29377  wlkres  29755  redwlk  29757  cyclnumvtx  29886  ofresid  32734  2ndresdju  32741  fdifsupp  32777  fdifsuppconst  32781  ressupprn  32782  fsuppcurry1  32816  fsuppcurry2  32817  mgcf1o  33082  gsumpart  33144  gsumhashmul  33148  tocyccntz  33225  elrspunsn  33512  ressply10g  33650  evls1subd  33655  ply1gsumz  33682  evlextv  33726  esplyind  33759  vietalem  33763  dimkerim  33811  irngss  33871  rtelextdg2lem  33910  zarcmplem  34065  measres  34406  ftc2re  34782  reprsuc  34799  bnj1379  35012  noinfepregs  35314  pfxwlk  35352  subgrwlk  35360  satom  35584  bj-fvsnun1  37615  evlselv  43039  fnwe2lem3  43497  wessf1ornlem  45632  limcperiod  46073  limclner  46094  limsupresxr  46209  liminfresxr  46210  cncfperiod  46322  sssmf  47181  fcores  47530  isubgrgrim  48420  rhmsubcALTVlem2  48773  tposidres  49376  oppff1  49638  oppff1o  49639  fuco11  49816  opf11  49893  opf12  49894  fucoppclem  49897  oppfdiag1a  49905  lmddu  50157