Theorem fvresd 6860

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↾ cres 5633  ‘cfv 6499

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-res 5643  df-iota 6452  df-fv 6507

This theorem is referenced by:  fvressn  7116  fvsnun1  7138  fvsnun2  7139  fsnunfv  7143  resfvresima  7191  ovres  7535  resf1extb  7890  curry1  8060  curry2  8063  frrlem4  8245  frrlem12  8253  smores  8298  smores2  8300  tz7.44-2  8352  seqomlem1  8395  seqomlem4  8398  onasuc  8469  onmsuc  8470  onesuc  8471  ordtypelem4  9450  ordtypelem6  9452  ordtypelem7  9453  unxpwdom2  9517  cantnfres  9606  cantnfp1lem3  9609  ttrclss  9649  dfac12lem1  10073  ackbij2lem2  10168  cfsmolem  10199  ttukeylem3  10440  fpwwe2lem5  10564  fpwwe2lem8  10567  canthp1lem2  10582  addpqnq  10867  mulpqnq  10870  seqf1olem2  13983  seqcoll  14405  rlimres  15500  lo1res  15501  isercolllem3  15609  ackbijnn  15770  bitsf1  16392  sadcaddlem  16403  sadaddlem  16412  sadasslem  16416  sadeq  16418  eucalgcvga  16532  eucalg  16533  funcres  17834  1stf1  18129  2ndf1  18132  1stfcl  18134  2ndfcl  18135  prf1st  18141  prf2nd  18142  1st2ndprf  18143  uncf2  18174  diag12  18181  diag2  18182  curf2ndf  18184  yonedalem22  18215  lubval  18291  glbval  18304  gsumsplit1r  18590  resmhm  18723  resghm  19140  efgsres  19644  efgredlemd  19650  efgredlem  19653  dprdres  19936  dmdprdsplit2lem  19953  rhmsubclem2  20571  imadrhmcl  20682  abvres  20716  reslmhm  20935  psgndiflemB  21485  evls1addd  22234  evls1muld  22235  evls1vsca  22236  evls1fvcl  22238  evls1maprhm  22239  evls1maprnss  22241  cnpresti  23151  cnprest  23152  upxp  23486  uptx  23488  txkgen  23515  remetdval  24653  lmcau  25189  dvreslem  25786  dvres2lem  25787  dvlip2  25876  c1liplem1  25877  dvgt0lem1  25883  lhop1lem  25894  dvcnvrelem1  25898  dvcvx  25901  psercn  26312  efcvx  26335  reefgim  26336  resinf1o  26421  efif1olem4  26430  eff1olem  26433  eflog  26461  logcn  26532  loglesqrt  26647  asinrebnd  26787  jensen  26875  amgmlem  26876  lgamgulmlem2  26916  mpodvdsmulf1o  27080  dvdsmulf1o  27082  dchrabs  27147  sum2dchr  27161  nolesgn2o  27559  nolesgn2ores  27560  nogesgn1o  27561  nogesgn1ores  27562  noresle  27585  nosupprefixmo  27588  noinfprefixmo  27589  nosupres  27595  nosupbnd2lem1  27603  noinfres  27610  noinfbnd2lem1  27618  noetasuplem4  27624  noetainflem4  27628  addsval  27845  mulsval  27988  onsiso  28145  uhgrspansubgrlem  29193  wlkres  29572  redwlk  29574  cyclnumvtx  29703  ofresid  32539  2ndresdju  32546  fdifsupp  32581  fdifsuppconst  32585  ressupprn  32586  fsuppcurry1  32621  fsuppcurry2  32622  mgcf1o  32902  gsumpart  32970  gsumhashmul  32974  tocyccntz  33074  elrspunsn  33373  ressply10g  33509  evls1subd  33514  ply1gsumz  33537  dimkerim  33596  irngss  33655  rtelextdg2lem  33689  zarcmplem  33844  measres  34185  ftc2re  34562  reprsuc  34579  bnj1379  34793  pfxwlk  35084  subgrwlk  35092  satom  35316  bj-fvsnun1  37216  selvvvval  42546  evlselv  42548  fnwe2lem3  43014  wessf1ornlem  45152  limcperiod  45599  limclner  45622  limsupresxr  45737  liminfresxr  45738  cncfperiod  45850  sssmf  46709  fcores  47041  isubgrgrim  47902  rhmsubcALTVlem2  48243  tposidres  48847  oppff1  49110  oppff1o  49111  fuco11  49288  opf11  49365  opf12  49366  fucoppclem  49369  oppfdiag1a  49377  lmddu  49629