Theorem fvresd 6926

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ↾ cres 5687  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-res 5697  df-iota 6514  df-fv 6569

This theorem is referenced by:  fvressn  7182  fvsnun1  7202  fvsnun2  7203  fsnunfv  7207  resfvresima  7255  ovres  7599  resf1extb  7956  curry1  8129  curry2  8132  frrlem4  8314  frrlem12  8322  smores  8392  smores2  8394  tz7.44-2  8447  seqomlem1  8490  seqomlem4  8493  onasuc  8566  onmsuc  8567  onesuc  8568  ordtypelem4  9561  ordtypelem6  9563  ordtypelem7  9564  unxpwdom2  9628  cantnfres  9717  cantnfp1lem3  9720  ttrclss  9760  dfac12lem1  10184  ackbij2lem2  10279  cfsmolem  10310  ttukeylem3  10551  fpwwe2lem5  10675  fpwwe2lem8  10678  canthp1lem2  10693  addpqnq  10978  mulpqnq  10981  seqf1olem2  14083  seqcoll  14503  rlimres  15594  lo1res  15595  isercolllem3  15703  ackbijnn  15864  bitsf1  16483  sadcaddlem  16494  sadaddlem  16503  sadasslem  16507  sadeq  16509  eucalgcvga  16623  eucalg  16624  funcres  17941  1stf1  18237  2ndf1  18240  1stfcl  18242  2ndfcl  18243  prf1st  18249  prf2nd  18250  1st2ndprf  18251  uncf2  18282  diag12  18289  diag2  18290  curf2ndf  18292  yonedalem22  18323  lubval  18401  glbval  18414  gsumsplit1r  18700  resmhm  18833  resghm  19250  efgsres  19756  efgredlemd  19762  efgredlem  19765  dprdres  20048  dmdprdsplit2lem  20065  rhmsubclem2  20686  imadrhmcl  20798  abvres  20832  reslmhm  21051  psgndiflemB  21618  evls1addd  22375  evls1muld  22376  evls1vsca  22377  evls1fvcl  22379  evls1maprhm  22380  evls1maprnss  22382  cnpresti  23296  cnprest  23297  upxp  23631  uptx  23633  txkgen  23660  remetdval  24810  lmcau  25347  dvreslem  25944  dvres2lem  25945  dvlip2  26034  c1liplem1  26035  dvgt0lem1  26041  lhop1lem  26052  dvcnvrelem1  26056  dvcvx  26059  psercn  26470  efcvx  26493  reefgim  26494  resinf1o  26578  efif1olem4  26587  eff1olem  26590  eflog  26618  logcn  26689  loglesqrt  26804  asinrebnd  26944  jensen  27032  amgmlem  27033  lgamgulmlem2  27073  mpodvdsmulf1o  27237  dvdsmulf1o  27239  dchrabs  27304  sum2dchr  27318  nolesgn2o  27716  nolesgn2ores  27717  nogesgn1o  27718  nogesgn1ores  27719  noresle  27742  nosupprefixmo  27745  noinfprefixmo  27746  nosupres  27752  nosupbnd2lem1  27760  noinfres  27767  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  addsval  27995  mulsval  28135  uhgrspansubgrlem  29307  wlkres  29688  redwlk  29690  cyclnumvtx  29820  ofresid  32652  2ndresdju  32659  fdifsupp  32694  fdifsuppconst  32698  ressupprn  32699  fsuppcurry1  32736  fsuppcurry2  32737  mgcf1o  32993  gsumpart  33060  gsumhashmul  33064  tocyccntz  33164  elrspunsn  33457  ressply10g  33592  evls1subd  33597  ply1gsumz  33619  dimkerim  33678  irngss  33737  rtelextdg2lem  33767  zarcmplem  33880  measres  34223  ftc2re  34613  reprsuc  34630  bnj1379  34844  pfxwlk  35129  subgrwlk  35137  satom  35361  bj-fvsnun1  37256  selvvvval  42595  evlselv  42597  fnwe2lem3  43064  wessf1ornlem  45190  limcperiod  45643  limclner  45666  limsupresxr  45781  liminfresxr  45782  cncfperiod  45894  sssmf  46753  fcores  47079  isubgrgrim  47897  rhmsubcALTVlem2  48198  tposidres  48786  fuco11  49021