Theorem fvresd 6862

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↾ cres 5634  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-res 5644  df-iota 6456  df-fv 6508

This theorem is referenced by:  fvressn  7117  fvsnun1  7138  fvsnun2  7139  fsnunfv  7143  resfvresima  7191  ovres  7534  resf1extb  7886  curry1  8056  curry2  8059  frrlem4  8241  frrlem12  8249  smores  8294  smores2  8296  tz7.44-2  8348  seqomlem1  8391  seqomlem4  8394  onasuc  8465  onmsuc  8466  onesuc  8467  ordtypelem4  9438  ordtypelem6  9440  ordtypelem7  9441  unxpwdom2  9505  cantnfres  9598  cantnfp1lem3  9601  ttrclss  9641  dfac12lem1  10066  ackbij2lem2  10161  cfsmolem  10192  ttukeylem3  10433  fpwwe2lem5  10558  fpwwe2lem8  10561  canthp1lem2  10576  addpqnq  10861  mulpqnq  10864  seqf1olem2  13977  seqcoll  14399  rlimres  15493  lo1res  15494  isercolllem3  15602  ackbijnn  15763  bitsf1  16385  sadcaddlem  16396  sadaddlem  16405  sadasslem  16409  sadeq  16411  eucalgcvga  16525  eucalg  16526  funcres  17832  1stf1  18127  2ndf1  18130  1stfcl  18132  2ndfcl  18133  prf1st  18139  prf2nd  18140  1st2ndprf  18141  uncf2  18172  diag12  18179  diag2  18180  curf2ndf  18182  yonedalem22  18213  lubval  18289  glbval  18302  gsumsplit1r  18624  resmhm  18757  resghm  19173  efgsres  19679  efgredlemd  19685  efgredlem  19688  dprdres  19971  dmdprdsplit2lem  19988  rhmsubclem2  20631  imadrhmcl  20742  abvres  20776  reslmhm  21016  psgndiflemB  21567  evls1addd  22327  evls1muld  22328  evls1vsca  22329  evls1fvcl  22331  evls1maprhm  22332  evls1maprnss  22334  cnpresti  23244  cnprest  23245  upxp  23579  uptx  23581  txkgen  23608  remetdval  24745  lmcau  25281  dvreslem  25878  dvres2lem  25879  dvlip2  25968  c1liplem1  25969  dvgt0lem1  25975  lhop1lem  25986  dvcnvrelem1  25990  dvcvx  25993  psercn  26404  efcvx  26427  reefgim  26428  resinf1o  26513  efif1olem4  26522  eff1olem  26525  eflog  26553  logcn  26624  loglesqrt  26739  asinrebnd  26879  jensen  26967  amgmlem  26968  lgamgulmlem2  27008  mpodvdsmulf1o  27172  dvdsmulf1o  27174  dchrabs  27239  sum2dchr  27253  nolesgn2o  27651  nolesgn2ores  27652  nogesgn1o  27653  nogesgn1ores  27654  noresle  27677  nosupprefixmo  27680  noinfprefixmo  27681  nosupres  27687  nosupbnd2lem1  27695  noinfres  27702  noinfbnd2lem1  27710  noetasuplem4  27716  noetainflem4  27720  addsval  27970  mulsval  28117  oniso  28279  addonbday  28287  bdayfinlem  28494  uhgrspansubgrlem  29375  wlkres  29754  redwlk  29756  cyclnumvtx  29885  ofresid  32732  2ndresdju  32739  fdifsupp  32775  fdifsuppconst  32779  ressupprn  32780  fsuppcurry1  32814  fsuppcurry2  32815  mgcf1o  33096  gsumpart  33157  gsumhashmul  33161  tocyccntz  33238  elrspunsn  33522  ressply10g  33660  evls1subd  33665  ply1gsumz  33692  evlextv  33719  esplyind  33752  vietalem  33756  dimkerim  33805  irngss  33865  rtelextdg2lem  33904  zarcmplem  34059  measres  34400  ftc2re  34776  reprsuc  34793  bnj1379  35006  noinfepregs  35311  pfxwlk  35340  subgrwlk  35348  satom  35572  bj-fvsnun1  37510  selvvvval  42943  evlselv  42945  fnwe2lem3  43409  wessf1ornlem  45544  limcperiod  45988  limclner  46009  limsupresxr  46124  liminfresxr  46125  cncfperiod  46237  sssmf  47096  fcores  47427  isubgrgrim  48289  rhmsubcALTVlem2  48642  tposidres  49245  oppff1  49507  oppff1o  49508  fuco11  49685  opf11  49762  opf12  49763  fucoppclem  49766  oppfdiag1a  49774  lmddu  50026