Theorem fvresd 6860

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↾ cres 5633  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-res 5643  df-iota 6452  df-fv 6507

This theorem is referenced by:  fvressn  7116  fvsnun1  7138  fvsnun2  7139  fsnunfv  7143  resfvresima  7191  ovres  7535  resf1extb  7890  curry1  8060  curry2  8063  frrlem4  8245  frrlem12  8253  smores  8298  smores2  8300  tz7.44-2  8352  seqomlem1  8395  seqomlem4  8398  onasuc  8469  onmsuc  8470  onesuc  8471  ordtypelem4  9450  ordtypelem6  9452  ordtypelem7  9453  unxpwdom2  9517  cantnfres  9606  cantnfp1lem3  9609  ttrclss  9649  dfac12lem1  10073  ackbij2lem2  10168  cfsmolem  10199  ttukeylem3  10440  fpwwe2lem5  10564  fpwwe2lem8  10567  canthp1lem2  10582  addpqnq  10867  mulpqnq  10870  seqf1olem2  13983  seqcoll  14405  rlimres  15500  lo1res  15501  isercolllem3  15609  ackbijnn  15770  bitsf1  16392  sadcaddlem  16403  sadaddlem  16412  sadasslem  16416  sadeq  16418  eucalgcvga  16532  eucalg  16533  funcres  17838  1stf1  18133  2ndf1  18136  1stfcl  18138  2ndfcl  18139  prf1st  18145  prf2nd  18146  1st2ndprf  18147  uncf2  18178  diag12  18185  diag2  18186  curf2ndf  18188  yonedalem22  18219  lubval  18295  glbval  18308  gsumsplit1r  18596  resmhm  18729  resghm  19146  efgsres  19652  efgredlemd  19658  efgredlem  19661  dprdres  19944  dmdprdsplit2lem  19961  rhmsubclem2  20606  imadrhmcl  20717  abvres  20751  reslmhm  20991  psgndiflemB  21542  evls1addd  22291  evls1muld  22292  evls1vsca  22293  evls1fvcl  22295  evls1maprhm  22296  evls1maprnss  22298  cnpresti  23208  cnprest  23209  upxp  23543  uptx  23545  txkgen  23572  remetdval  24710  lmcau  25246  dvreslem  25843  dvres2lem  25844  dvlip2  25933  c1liplem1  25934  dvgt0lem1  25940  lhop1lem  25951  dvcnvrelem1  25955  dvcvx  25958  psercn  26369  efcvx  26392  reefgim  26393  resinf1o  26478  efif1olem4  26487  eff1olem  26490  eflog  26518  logcn  26589  loglesqrt  26704  asinrebnd  26844  jensen  26932  amgmlem  26933  lgamgulmlem2  26973  mpodvdsmulf1o  27137  dvdsmulf1o  27139  dchrabs  27204  sum2dchr  27218  nolesgn2o  27616  nolesgn2ores  27617  nogesgn1o  27618  nogesgn1ores  27619  noresle  27642  nosupprefixmo  27645  noinfprefixmo  27646  nosupres  27652  nosupbnd2lem1  27660  noinfres  27667  noinfbnd2lem1  27675  noetasuplem4  27681  noetainflem4  27685  addsval  27909  mulsval  28052  onsiso  28209  uhgrspansubgrlem  29270  wlkres  29649  redwlk  29651  cyclnumvtx  29780  ofresid  32616  2ndresdju  32623  fdifsupp  32658  fdifsuppconst  32662  ressupprn  32663  fsuppcurry1  32698  fsuppcurry2  32699  mgcf1o  32975  gsumpart  33040  gsumhashmul  33044  tocyccntz  33116  elrspunsn  33393  ressply10g  33529  evls1subd  33534  ply1gsumz  33557  dimkerim  33616  irngss  33675  rtelextdg2lem  33709  zarcmplem  33864  measres  34205  ftc2re  34582  reprsuc  34599  bnj1379  34813  pfxwlk  35104  subgrwlk  35112  satom  35336  bj-fvsnun1  37236  selvvvval  42566  evlselv  42568  fnwe2lem3  43034  wessf1ornlem  45172  limcperiod  45619  limclner  45642  limsupresxr  45757  liminfresxr  45758  cncfperiod  45870  sssmf  46729  fcores  47061  isubgrgrim  47922  rhmsubcALTVlem2  48263  tposidres  48867  oppff1  49130  oppff1o  49131  fuco11  49308  opf11  49385  opf12  49386  fucoppclem  49389  oppfdiag1a  49397  lmddu  49649