Theorem fvresd 6854

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ↾ cres 5626  ‘cfv 6492

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-res 5636  df-iota 6448  df-fv 6500

This theorem is referenced by:  fvressn  7107  fvsnun1  7128  fvsnun2  7129  fsnunfv  7133  resfvresima  7181  ovres  7524  resf1extb  7876  curry1  8046  curry2  8049  frrlem4  8231  frrlem12  8239  smores  8284  smores2  8286  tz7.44-2  8338  seqomlem1  8381  seqomlem4  8384  onasuc  8455  onmsuc  8456  onesuc  8457  ordtypelem4  9426  ordtypelem6  9428  ordtypelem7  9429  unxpwdom2  9493  cantnfres  9586  cantnfp1lem3  9589  ttrclss  9629  dfac12lem1  10054  ackbij2lem2  10149  cfsmolem  10180  ttukeylem3  10421  fpwwe2lem5  10546  fpwwe2lem8  10549  canthp1lem2  10564  addpqnq  10849  mulpqnq  10852  seqf1olem2  13965  seqcoll  14387  rlimres  15481  lo1res  15482  isercolllem3  15590  ackbijnn  15751  bitsf1  16373  sadcaddlem  16384  sadaddlem  16393  sadasslem  16397  sadeq  16399  eucalgcvga  16513  eucalg  16514  funcres  17820  1stf1  18115  2ndf1  18118  1stfcl  18120  2ndfcl  18121  prf1st  18127  prf2nd  18128  1st2ndprf  18129  uncf2  18160  diag12  18167  diag2  18168  curf2ndf  18170  yonedalem22  18201  lubval  18277  glbval  18290  gsumsplit1r  18612  resmhm  18745  resghm  19161  efgsres  19667  efgredlemd  19673  efgredlem  19676  dprdres  19959  dmdprdsplit2lem  19976  rhmsubclem2  20619  imadrhmcl  20730  abvres  20764  reslmhm  21004  psgndiflemB  21555  evls1addd  22315  evls1muld  22316  evls1vsca  22317  evls1fvcl  22319  evls1maprhm  22320  evls1maprnss  22322  cnpresti  23232  cnprest  23233  upxp  23567  uptx  23569  txkgen  23596  remetdval  24733  lmcau  25269  dvreslem  25866  dvres2lem  25867  dvlip2  25956  c1liplem1  25957  dvgt0lem1  25963  lhop1lem  25974  dvcnvrelem1  25978  dvcvx  25981  psercn  26392  efcvx  26415  reefgim  26416  resinf1o  26501  efif1olem4  26510  eff1olem  26513  eflog  26541  logcn  26612  loglesqrt  26727  asinrebnd  26867  jensen  26955  amgmlem  26956  lgamgulmlem2  26996  mpodvdsmulf1o  27160  dvdsmulf1o  27162  dchrabs  27227  sum2dchr  27241  nolesgn2o  27639  nolesgn2ores  27640  nogesgn1o  27641  nogesgn1ores  27642  noresle  27665  nosupprefixmo  27668  noinfprefixmo  27669  nosupres  27675  nosupbnd2lem1  27683  noinfres  27690  noinfbnd2lem1  27698  noetasuplem4  27704  noetainflem4  27708  addsval  27958  mulsval  28105  oniso  28267  addonbday  28275  bdayfinlem  28482  uhgrspansubgrlem  29363  wlkres  29742  redwlk  29744  cyclnumvtx  29873  ofresid  32720  2ndresdju  32727  fdifsupp  32764  fdifsuppconst  32768  ressupprn  32769  fsuppcurry1  32803  fsuppcurry2  32804  mgcf1o  33085  gsumpart  33146  gsumhashmul  33150  tocyccntz  33226  elrspunsn  33510  ressply10g  33648  evls1subd  33653  ply1gsumz  33680  evlextv  33707  esplyind  33731  vietalem  33735  dimkerim  33784  irngss  33844  rtelextdg2lem  33883  zarcmplem  34038  measres  34379  ftc2re  34755  reprsuc  34772  bnj1379  34986  noinfepregs  35289  pfxwlk  35318  subgrwlk  35326  satom  35550  bj-fvsnun1  37460  selvvvval  42828  evlselv  42830  fnwe2lem3  43294  wessf1ornlem  45429  limcperiod  45874  limclner  45895  limsupresxr  46010  liminfresxr  46011  cncfperiod  46123  sssmf  46982  fcores  47313  isubgrgrim  48175  rhmsubcALTVlem2  48528  tposidres  49131  oppff1  49393  oppff1o  49394  fuco11  49571  opf11  49648  opf12  49649  fucoppclem  49652  oppfdiag1a  49660  lmddu  49912