Theorem fvresd 6842

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ↾ cres 5616  ‘cfv 6481

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-xp 5620  df-res 5626  df-iota 6437  df-fv 6489

This theorem is referenced by:  fvressn  7095  fvsnun1  7116  fvsnun2  7117  fsnunfv  7121  resfvresima  7169  ovres  7512  resf1extb  7864  curry1  8034  curry2  8037  frrlem4  8219  frrlem12  8227  smores  8272  smores2  8274  tz7.44-2  8326  seqomlem1  8369  seqomlem4  8372  onasuc  8443  onmsuc  8444  onesuc  8445  ordtypelem4  9407  ordtypelem6  9409  ordtypelem7  9410  unxpwdom2  9474  cantnfres  9567  cantnfp1lem3  9570  ttrclss  9610  dfac12lem1  10035  ackbij2lem2  10130  cfsmolem  10161  ttukeylem3  10402  fpwwe2lem5  10526  fpwwe2lem8  10529  canthp1lem2  10544  addpqnq  10829  mulpqnq  10832  seqf1olem2  13949  seqcoll  14371  rlimres  15465  lo1res  15466  isercolllem3  15574  ackbijnn  15735  bitsf1  16357  sadcaddlem  16368  sadaddlem  16377  sadasslem  16381  sadeq  16383  eucalgcvga  16497  eucalg  16498  funcres  17803  1stf1  18098  2ndf1  18101  1stfcl  18103  2ndfcl  18104  prf1st  18110  prf2nd  18111  1st2ndprf  18112  uncf2  18143  diag12  18150  diag2  18151  curf2ndf  18153  yonedalem22  18184  lubval  18260  glbval  18273  gsumsplit1r  18595  resmhm  18728  resghm  19144  efgsres  19650  efgredlemd  19656  efgredlem  19659  dprdres  19942  dmdprdsplit2lem  19959  rhmsubclem2  20601  imadrhmcl  20712  abvres  20746  reslmhm  20986  psgndiflemB  21537  evls1addd  22286  evls1muld  22287  evls1vsca  22288  evls1fvcl  22290  evls1maprhm  22291  evls1maprnss  22293  cnpresti  23203  cnprest  23204  upxp  23538  uptx  23540  txkgen  23567  remetdval  24704  lmcau  25240  dvreslem  25837  dvres2lem  25838  dvlip2  25927  c1liplem1  25928  dvgt0lem1  25934  lhop1lem  25945  dvcnvrelem1  25949  dvcvx  25952  psercn  26363  efcvx  26386  reefgim  26387  resinf1o  26472  efif1olem4  26481  eff1olem  26484  eflog  26512  logcn  26583  loglesqrt  26698  asinrebnd  26838  jensen  26926  amgmlem  26927  lgamgulmlem2  26967  mpodvdsmulf1o  27131  dvdsmulf1o  27133  dchrabs  27198  sum2dchr  27212  nolesgn2o  27610  nolesgn2ores  27611  nogesgn1o  27612  nogesgn1ores  27613  noresle  27636  nosupprefixmo  27639  noinfprefixmo  27640  nosupres  27646  nosupbnd2lem1  27654  noinfres  27661  noinfbnd2lem1  27669  noetasuplem4  27675  noetainflem4  27679  addsval  27905  mulsval  28048  onsiso  28205  uhgrspansubgrlem  29268  wlkres  29647  redwlk  29649  cyclnumvtx  29778  ofresid  32624  2ndresdju  32631  fdifsupp  32666  fdifsuppconst  32670  ressupprn  32671  fsuppcurry1  32707  fsuppcurry2  32708  mgcf1o  32984  gsumpart  33037  gsumhashmul  33041  tocyccntz  33113  elrspunsn  33394  ressply10g  33530  evls1subd  33535  ply1gsumz  33559  dimkerim  33640  irngss  33700  rtelextdg2lem  33739  zarcmplem  33894  measres  34235  ftc2re  34611  reprsuc  34628  bnj1379  34842  pfxwlk  35168  subgrwlk  35176  satom  35400  bj-fvsnun1  37297  selvvvval  42626  evlselv  42628  fnwe2lem3  43093  wessf1ornlem  45230  limcperiod  45676  limclner  45697  limsupresxr  45812  liminfresxr  45813  cncfperiod  45925  sssmf  46784  fcores  47106  isubgrgrim  47968  rhmsubcALTVlem2  48321  tposidres  48925  oppff1  49188  oppff1o  49189  fuco11  49366  opf11  49443  opf12  49444  fucoppclem  49447  oppfdiag1a  49455  lmddu  49707