Theorem fvresd 6887

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142   ↾ cres 5649  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-res 5659  df-iota 6477  df-fv 6529

This theorem is referenced by:  fvressn  7145  fvsnun1  7166  fvsnun2  7167  fsnunfv  7171  resfvresima  7219  ovres  7562  resf1extb  7915  curry1  8083  curry2  8086  frrlem4  8270  frrlem12  8278  smores  8323  smores2  8325  tz7.44-2  8378  seqomlem1  8421  seqomlem4  8424  onasuc  8497  onmsuc  8498  onesuc  8499  ordtypelem4  9469  ordtypelem6  9471  ordtypelem7  9472  unxpwdom2  9536  cantnfres  9632  cantnfp1lem3  9635  ttrclss  9675  dfac12lem1  10100  ackbij2lem2  10195  cfsmolem  10227  ttukeylem3  10468  fpwwe2lem5  10593  fpwwe2lem8  10596  canthp1lem2  10611  addpqnq  10896  mulpqnq  10899  seqf1olem2  14055  seqcoll  14477  rlimres  15585  lo1res  15586  isercolllem3  15694  ackbijnn  15858  bitsf1  16480  sadcaddlem  16491  sadaddlem  16500  sadasslem  16504  sadeq  16506  eucalgcvga  16620  eucalg  16621  funcres  17929  1stf1  18224  2ndf1  18227  1stfcl  18229  2ndfcl  18230  prf1st  18236  prf2nd  18237  1st2ndprf  18238  uncf2  18269  diag12  18276  diag2  18277  curf2ndf  18279  yonedalem22  18310  lubval  18386  glbval  18399  gsumsplit1r  18721  resmhm  18854  resghm  19272  efgsres  19778  efgredlemd  19784  efgredlem  19787  dprdres  20070  dmdprdsplit2lem  20087  rhmsubclem2  20732  imadrhmcl  20843  abvres  20877  reslmhm  21116  psgndiflemB  21649  selvvvval  22192  evls1addd  22431  evls1muld  22432  evls1vsca  22433  evls1fvcl  22435  evls1maprhm  22436  evls1maprnss  22438  cnpresti  23345  cnprest  23346  upxp  23680  uptx  23682  txkgen  23709  remetdval  24846  lmcau  25372  dvreslem  25968  dvres2lem  25969  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  lhop1lem  26072  dvcnvrelem1  26076  dvcvx  26079  psercn  26486  efcvx  26509  reefgim  26510  resinf1o  26598  efif1olem4  26607  eff1olem  26610  eflog  26638  logcn  26709  loglesqrt  26823  asinrebnd  26963  jensen  27050  amgmlem  27051  lgamgulmlem2  27091  mpodvdsmulf1o  27255  dvdsmulf1o  27257  dchrabs  27321  sum2dchr  27335  nolesgn2o  27732  nolesgn2ores  27733  nogesgn1o  27734  nogesgn1ores  27735  noresle  27758  nosupprefixmo  27761  noinfprefixmo  27762  nosupres  27768  nosupbnd2lem1  27776  noinfres  27783  noinfbnd2lem1  27791  noetasuplem4  27797  noetainflem4  27801  addsval  28052  mulsval  28199  oniso  28361  addonbday  28369  bdayfinlem  28576  uhgrspansubgrlem  29488  wlkres  29866  redwlk  29868  cyclnumvtx  29997  ofresid  32841  2ndresdju  32848  fdifsupp  32884  fdifsuppconst  32888  ressupprn  32889  fsuppcurry1  32923  fsuppcurry2  32924  mgcf1o  33178  gsumpart  33240  gsumhashmul  33244  tocyccntz  33321  elrspunsn  33612  ressply10g  33760  evls1subd  33765  ply1gsumz  33792  evlextv  33836  esplyind  33869  vietalem  33873  dimkerim  33921  irngss  33981  rtelextdg2lem  34020  zarcmplem  34175  measres  34516  ftc2re  34889  reprsuc  34906  bnj1379  35122  noinfepregs  35426  pfxwlk  35471  subgrwlk  35479  satom  35703  nmulprop  36537  bj-fvsnun1  37744  evlselv  43168  fnwe2lem3  43626  wessf1ornlem  45760  limcperiod  46201  limclner  46222  limsupresxr  46337  liminfresxr  46338  cncfperiod  46450  sssmf  47309  fcores  47658  isubgrgrim  48548  rhmsubcALTVlem2  48901  tposidres  49504  oppff1  49766  oppff1o  49767  fuco11  49944  opf11  50021  opf12  50022  fucoppclem  50025  oppfdiag1a  50033  lmddu  50285