Theorem fvresd 6852

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ↾ cres 5624  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-res 5634  df-iota 6446  df-fv 6498

This theorem is referenced by:  fvressn  7105  fvsnun1  7126  fvsnun2  7127  fsnunfv  7131  resfvresima  7179  ovres  7522  resf1extb  7874  curry1  8044  curry2  8047  frrlem4  8229  frrlem12  8237  smores  8282  smores2  8284  tz7.44-2  8336  seqomlem1  8379  seqomlem4  8382  onasuc  8453  onmsuc  8454  onesuc  8455  ordtypelem4  9424  ordtypelem6  9426  ordtypelem7  9427  unxpwdom2  9491  cantnfres  9584  cantnfp1lem3  9587  ttrclss  9627  dfac12lem1  10052  ackbij2lem2  10147  cfsmolem  10178  ttukeylem3  10419  fpwwe2lem5  10544  fpwwe2lem8  10547  canthp1lem2  10562  addpqnq  10847  mulpqnq  10850  seqf1olem2  13963  seqcoll  14385  rlimres  15479  lo1res  15480  isercolllem3  15588  ackbijnn  15749  bitsf1  16371  sadcaddlem  16382  sadaddlem  16391  sadasslem  16395  sadeq  16397  eucalgcvga  16511  eucalg  16512  funcres  17818  1stf1  18113  2ndf1  18116  1stfcl  18118  2ndfcl  18119  prf1st  18125  prf2nd  18126  1st2ndprf  18127  uncf2  18158  diag12  18165  diag2  18166  curf2ndf  18168  yonedalem22  18199  lubval  18275  glbval  18288  gsumsplit1r  18610  resmhm  18743  resghm  19159  efgsres  19665  efgredlemd  19671  efgredlem  19674  dprdres  19957  dmdprdsplit2lem  19974  rhmsubclem2  20617  imadrhmcl  20728  abvres  20762  reslmhm  21002  psgndiflemB  21553  evls1addd  22313  evls1muld  22314  evls1vsca  22315  evls1fvcl  22317  evls1maprhm  22318  evls1maprnss  22320  cnpresti  23230  cnprest  23231  upxp  23565  uptx  23567  txkgen  23594  remetdval  24731  lmcau  25267  dvreslem  25864  dvres2lem  25865  dvlip2  25954  c1liplem1  25955  dvgt0lem1  25961  lhop1lem  25972  dvcnvrelem1  25976  dvcvx  25979  psercn  26390  efcvx  26413  reefgim  26414  resinf1o  26499  efif1olem4  26508  eff1olem  26511  eflog  26539  logcn  26610  loglesqrt  26725  asinrebnd  26865  jensen  26953  amgmlem  26954  lgamgulmlem2  26994  mpodvdsmulf1o  27158  dvdsmulf1o  27160  dchrabs  27225  sum2dchr  27239  nolesgn2o  27637  nolesgn2ores  27638  nogesgn1o  27639  nogesgn1ores  27640  noresle  27663  nosupprefixmo  27666  noinfprefixmo  27667  nosupres  27673  nosupbnd2lem1  27681  noinfres  27688  noinfbnd2lem1  27696  noetasuplem4  27702  noetainflem4  27706  addsval  27932  mulsval  28078  onsiso  28236  uhgrspansubgrlem  29312  wlkres  29691  redwlk  29693  cyclnumvtx  29822  ofresid  32669  2ndresdju  32676  fdifsupp  32713  fdifsuppconst  32717  ressupprn  32718  fsuppcurry1  32752  fsuppcurry2  32753  mgcf1o  33034  gsumpart  33095  gsumhashmul  33099  tocyccntz  33175  elrspunsn  33459  ressply10g  33597  evls1subd  33602  ply1gsumz  33629  evlextv  33656  esplyind  33680  vietalem  33684  dimkerim  33733  irngss  33793  rtelextdg2lem  33832  zarcmplem  33987  measres  34328  ftc2re  34704  reprsuc  34721  bnj1379  34935  noinfepregs  35238  pfxwlk  35267  subgrwlk  35275  satom  35499  bj-fvsnun1  37399  selvvvval  42770  evlselv  42772  fnwe2lem3  43236  wessf1ornlem  45371  limcperiod  45816  limclner  45837  limsupresxr  45952  liminfresxr  45953  cncfperiod  46065  sssmf  46924  fcores  47255  isubgrgrim  48117  rhmsubcALTVlem2  48470  tposidres  49073  oppff1  49335  oppff1o  49336  fuco11  49513  opf11  49590  opf12  49591  fucoppclem  49594  oppfdiag1a  49602  lmddu  49854