Theorem fvresd 6878

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

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

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-res 5650  df-iota 6464  df-fv 6519

This theorem is referenced by:  fvressn  7134  fvsnun1  7156  fvsnun2  7157  fsnunfv  7161  resfvresima  7209  ovres  7555  resf1extb  7910  curry1  8083  curry2  8086  frrlem4  8268  frrlem12  8276  smores  8321  smores2  8323  tz7.44-2  8375  seqomlem1  8418  seqomlem4  8421  onasuc  8492  onmsuc  8493  onesuc  8494  ordtypelem4  9474  ordtypelem6  9476  ordtypelem7  9477  unxpwdom2  9541  cantnfres  9630  cantnfp1lem3  9633  ttrclss  9673  dfac12lem1  10097  ackbij2lem2  10192  cfsmolem  10223  ttukeylem3  10464  fpwwe2lem5  10588  fpwwe2lem8  10591  canthp1lem2  10606  addpqnq  10891  mulpqnq  10894  seqf1olem2  14007  seqcoll  14429  rlimres  15524  lo1res  15525  isercolllem3  15633  ackbijnn  15794  bitsf1  16416  sadcaddlem  16427  sadaddlem  16436  sadasslem  16440  sadeq  16442  eucalgcvga  16556  eucalg  16557  funcres  17858  1stf1  18153  2ndf1  18156  1stfcl  18158  2ndfcl  18159  prf1st  18165  prf2nd  18166  1st2ndprf  18167  uncf2  18198  diag12  18205  diag2  18206  curf2ndf  18208  yonedalem22  18239  lubval  18315  glbval  18328  gsumsplit1r  18614  resmhm  18747  resghm  19164  efgsres  19668  efgredlemd  19674  efgredlem  19677  dprdres  19960  dmdprdsplit2lem  19977  rhmsubclem2  20595  imadrhmcl  20706  abvres  20740  reslmhm  20959  psgndiflemB  21509  evls1addd  22258  evls1muld  22259  evls1vsca  22260  evls1fvcl  22262  evls1maprhm  22263  evls1maprnss  22265  cnpresti  23175  cnprest  23176  upxp  23510  uptx  23512  txkgen  23539  remetdval  24677  lmcau  25213  dvreslem  25810  dvres2lem  25811  dvlip2  25900  c1liplem1  25901  dvgt0lem1  25907  lhop1lem  25918  dvcnvrelem1  25922  dvcvx  25925  psercn  26336  efcvx  26359  reefgim  26360  resinf1o  26445  efif1olem4  26454  eff1olem  26457  eflog  26485  logcn  26556  loglesqrt  26671  asinrebnd  26811  jensen  26899  amgmlem  26900  lgamgulmlem2  26940  mpodvdsmulf1o  27104  dvdsmulf1o  27106  dchrabs  27171  sum2dchr  27185  nolesgn2o  27583  nolesgn2ores  27584  nogesgn1o  27585  nogesgn1ores  27586  noresle  27609  nosupprefixmo  27612  noinfprefixmo  27613  nosupres  27619  nosupbnd2lem1  27627  noinfres  27634  noinfbnd2lem1  27642  noetasuplem4  27648  noetainflem4  27652  addsval  27869  mulsval  28012  onsiso  28169  uhgrspansubgrlem  29217  wlkres  29598  redwlk  29600  cyclnumvtx  29730  ofresid  32566  2ndresdju  32573  fdifsupp  32608  fdifsuppconst  32612  ressupprn  32613  fsuppcurry1  32648  fsuppcurry2  32649  mgcf1o  32929  gsumpart  32997  gsumhashmul  33001  tocyccntz  33101  elrspunsn  33400  ressply10g  33536  evls1subd  33541  ply1gsumz  33564  dimkerim  33623  irngss  33682  rtelextdg2lem  33716  zarcmplem  33871  measres  34212  ftc2re  34589  reprsuc  34606  bnj1379  34820  pfxwlk  35111  subgrwlk  35119  satom  35343  bj-fvsnun1  37243  selvvvval  42573  evlselv  42575  fnwe2lem3  43041  wessf1ornlem  45179  limcperiod  45626  limclner  45649  limsupresxr  45764  liminfresxr  45765  cncfperiod  45877  sssmf  46736  fcores  47068  isubgrgrim  47929  rhmsubcALTVlem2  48270  tposidres  48874  oppff1  49137  oppff1o  49138  fuco11  49315  opf11  49392  opf12  49393  fucoppclem  49396  oppfdiag1a  49404  lmddu  49656