Theorem fvresd 6910

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ↾ cres 5653  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5657  df-res 5663  df-iota 6497  df-fv 6551

This theorem is used by:  fvressn  7171  fvsnun1  7191  fvsnun2  7192  fsnunfv  7196  resfvresima  7245  ovres  7590  resf1extb  7950  curry1  8121  curry2  8124  fnwe2lem4  8154  frrlem4  8314  frrlem12  8322  smores  8367  smores2  8369  tz7.44-2  8422  seqomlem1  8467  seqomlem4  8470  onasuc  8543  onmsuc  8544  onesuc  8545  ordtypelem4  9522  ordtypelem6  9524  ordtypelem7  9525  unxpwdom2  9589  cantnfres  9685  cantnfp1lem3  9688  ttrclss  9728  dfac12lem1  10229  ackbij2lem2  10324  cfsmolem  10355  ttukeylem3  10596  fpwwe2lem5  10727  fpwwe2lem8  10730  canthp1lem2  10745  addpqnq  11030  mulpqnq  11033  seqf1olem2  14192  seqcoll  14616  rlimres  15734  lo1res  15735  isercolllem3  15843  ackbijnn  16006  bitsf1  16625  sadcaddlem  16636  sadaddlem  16645  sadasslem  16649  sadeq  16651  eucalgcvga  16770  eucalg  16771  funcres  18080  1stf1  18375  2ndf1  18378  1stfcl  18380  2ndfcl  18381  prf1st  18387  prf2nd  18388  1st2ndprf  18389  uncf2  18420  diag12  18427  diag2  18428  curf2ndf  18430  yonedalem22  18461  lubval  18537  glbval  18550  mgmn0plusgplusf  18837  gsumsplit1r  18885  resmhm  19025  resghm  19455  efgsres  19961  efgredlemd  19967  efgredlem  19970  dprdres  20253  dmdprdsplit2lem  20270  rhmsubclem2  20947  imadrhmcl  21063  abvres  21097  reslmhm  21336  psgndiflemB  21915  selvvvval  22460  evls1addd  22698  evls1muld  22699  evls1vsca  22700  evls1fvcl  22702  evls1maprhm  22703  evls1maprnss  22705  cnpresti  23615  cnprest  23616  upxp  23951  uptx  23953  txkgen  23980  remetdval  25117  lmcau  25643  dvreslem  26238  dvres2lem  26239  dvlip2  26324  c1liplem1  26325  dvgt0lem1  26331  lhop1lem  26342  dvcnvrelem1  26346  dvcvx  26349  psercn  26762  efcvx  26785  reefgim  26786  resinf1o  26873  efif1olem4  26882  eff1olem  26885  eflog  26913  logcn  26984  loglesqrt  27098  asinrebnd  27238  jensen  27325  amgmlem  27326  lgamgulmlem2  27366  mpodvdsmulf1o  27530  dvdsmulf1o  27532  dchrabs  27596  sum2dchr  27610  nolesgn2o  28037  nolesgn2ores  28038  nogesgn1o  28039  nogesgn1ores  28040  noresle  28063  nosupprefixmo  28066  noinfprefixmo  28067  nosupres  28073  nosupbnd2lem1  28081  noinfres  28088  noinfbnd2lem1  28096  noetasuplem4  28102  noetainflem4  28106  addsval  28357  mulsval  28504  oniso  28666  addonbday  28674  bdayfinlem  28881  uhgrspansubgrlem  29880  wlkres  30258  redwlk  30260  pfxwlk  30275  subgrwlk  30278  cyclnumvtx  30397  foresf1o  33151  ofresid  33287  2ndresdju  33294  fdifsupp  33329  fdifsuppconst  33333  ressupprn  33334  fsuppcurry1  33366  fsuppcurry2  33367  mgcf1o  33614  gsumpart  33674  gsumhashmul  33678  tocyccntz  33755  elrspunsn  34029  ressply10g  34149  evls1subd  34154  ply1gsumz  34181  evlextv  34224  esplyind  34257  vietalem  34261  dimkerim  34309  irngss  34369  rtelextdg2lem  34408  zarcmplem  34563  measres  34905  ftc2re  35277  reprsuc  35294  bnj1379  35510  noinfepregs  35861  satom  36211  nmulprop  37035  bj-fvsnun1  38285  evlselv  43726  hashnna  46117  wessf1ornlem  46308  limcperiod  46748  limclner  46769  limsupresxr  46884  liminfresxr  46885  cncfperiod  46997  sssmf  47856  fcores  48245  isubgrgrim  49135  rhmsubcALTVlem2  49487  tposidres  50107  oppff1  50372  oppff1o  50373  fuco11  50556  opf11  50646  opf12  50647  fucoppclem  50650  oppfdiag1a  50658  lmddu  50958