Theorem fvresd 6683

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ↾ cres 5530  ‘cfv 6340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-xp 5534  df-res 5540  df-iota 6299  df-fv 6348

This theorem is referenced by:  fvressn  6921  fvsnun1  6941  fvsnun2  6942  fsnunfv  6946  resfvresima  6995  ovres  7316  curry1  7810  curry2  7813  smores  8005  smores2  8007  tz7.44-2  8059  seqomlem1  8102  seqomlem4  8105  onasuc  8169  onmsuc  8170  onesuc  8171  ordtypelem4  9031  ordtypelem6  9033  ordtypelem7  9034  unxpwdom2  9098  cantnfres  9186  cantnfp1lem3  9189  dfac12lem1  9616  ackbij2lem2  9713  cfsmolem  9743  ttukeylem3  9984  fpwwe2lem5  10108  fpwwe2lem8  10111  canthp1lem2  10126  addpqnq  10411  mulpqnq  10414  seqf1olem2  13473  seqcoll  13887  rlimres  14976  lo1res  14977  isercolllem3  15084  ackbijnn  15244  bitsf1  15858  sadcaddlem  15869  sadaddlem  15878  sadasslem  15882  sadeq  15884  eucalgcvga  15995  eucalg  15996  funcres  17238  1stf1  17521  2ndf1  17524  1stfcl  17526  2ndfcl  17527  prf1st  17533  prf2nd  17534  1st2ndprf  17535  uncf2  17566  diag12  17573  diag2  17574  curf2ndf  17576  yonedalem22  17607  lubval  17673  glbval  17686  gsumsplit1r  17976  resmhm  18064  resghm  18454  efgsres  18944  efgredlemd  18950  efgredlem  18953  dprdres  19231  dmdprdsplit2lem  19248  abvres  19691  reslmhm  19905  psgndiflemB  20378  cnpresti  22001  cnprest  22002  upxp  22336  uptx  22338  txkgen  22365  remetdval  23503  lmcau  24026  dvreslem  24621  dvres2lem  24622  dvlip2  24707  c1liplem1  24708  dvgt0lem1  24714  lhop1lem  24725  dvcnvrelem1  24729  dvcvx  24732  psercn  25133  efcvx  25156  reefgim  25157  resinf1o  25240  efif1olem4  25249  eff1olem  25252  eflog  25280  logcn  25350  loglesqrt  25459  asinrebnd  25599  jensen  25686  amgmlem  25687  lgamgulmlem2  25727  dvdsmulf1o  25891  dchrabs  25956  sum2dchr  25970  uhgrspansubgrlem  27192  wlkres  27572  redwlk  27574  ofresid  30514  2ndresdju  30521  fdifsuppconst  30559  ressupprn  30560  fsuppcurry1  30596  fsuppcurry2  30597  mgcf1o  30819  gsumpart  30853  gsumhashmul  30854  tocyccntz  30949  dimkerim  31241  zarcmplem  31364  measres  31721  ftc2re  32109  reprsuc  32126  bnj1379  32342  pfxwlk  32613  subgrwlk  32622  satom  32846  frrlem4  33400  frrlem12  33408  nolesgn2o  33471  nolesgn2ores  33472  nogesgn1o  33473  nogesgn1ores  33474  noresle  33497  nosupprefixmo  33500  noinfprefixmo  33501  nosupres  33507  nosupbnd2lem1  33515  noinfres  33522  noinfbnd2lem1  33530  noetasuplem4  33536  noetainflem4  33540  addsov  33709  bj-fvsnun1  34984  fnwe2lem3  40404  wessf1ornlem  42216  limcperiod  42671  limclner  42694  limsupresxr  42809  liminfresxr  42810  cncfperiod  42922  sssmf  43773  rhmsubclem2  45127  rhmsubcALTVlem2  45145