Theorem fvresd 6936

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ↾ cres 5660  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-res 5670  df-iota 6520  df-fv 6574

This theorem is used by:  fvressn  7198  fvsnun1  7218  fvsnun2  7219  fsnunfv  7223  resfvresima  7272  ovres  7618  resf1extb  7980  curry1  8152  curry2  8155  fnwe2lem4  8185  frrlem4  8345  frrlem12  8353  smores  8398  smores2  8400  tz7.44-2  8453  seqomlem1  8498  seqomlem4  8501  onasuc  8574  onmsuc  8575  onesuc  8576  ordtypelem4  9552  ordtypelem6  9554  ordtypelem7  9555  unxpwdom2  9619  cantnfres  9715  cantnfp1lem3  9718  ttrclss  9758  dfac12lem1  10261  ackbij2lem2  10356  cfsmolem  10387  ttukeylem3  10628  fpwwe2lem5  10759  fpwwe2lem8  10762  canthp1lem2  10777  addpqnq  11062  mulpqnq  11065  seqf1olem2  14225  seqcoll  14650  rlimres  15769  lo1res  15770  isercolllem3  15878  ackbijnn  16041  bitsf1  16660  sadcaddlem  16671  sadaddlem  16680  sadasslem  16684  sadeq  16686  eucalgcvga  16805  eucalg  16806  funcres  18121  1stf1  18416  2ndf1  18419  1stfcl  18421  2ndfcl  18422  prf1st  18428  prf2nd  18429  1st2ndprf  18430  uncf2  18461  diag12  18468  diag2  18469  curf2ndf  18471  yonedalem22  18502  lubval  18578  glbval  18591  mgmn0plusgplusf  18878  gsumsplit1r  18926  resmhm  19066  resghm  19496  efgsres  20003  efgredlemd  20009  efgredlem  20012  dprdres  20295  dmdprdsplit2lem  20312  rhmsubclem2  20989  imadrhmcl  21105  abvres  21139  reslmhm  21378  psgndiflemB  21961  selvvvval  22506  evls1addd  22744  evls1muld  22745  evls1vsca  22746  evls1fvcl  22748  evls1maprhm  22749  evls1maprnss  22751  cnpresti  23661  cnprest  23662  upxp  23997  uptx  23999  txkgen  24026  remetdval  25163  lmcau  25689  dvreslem  26284  dvres2lem  26285  dvlip2  26370  c1liplem1  26371  dvgt0lem1  26377  lhop1lem  26388  dvcnvrelem1  26392  dvcvx  26395  psercn  26810  efcvx  26833  reefgim  26834  resinf1o  26921  efif1olem4  26930  eff1olem  26933  eflog  26961  logcn  27032  loglesqrt  27146  asinrebnd  27286  jensen  27373  amgmlem  27374  lgamgulmlem2  27414  mpodvdsmulf1o  27578  dvdsmulf1o  27580  dchrabs  27644  sum2dchr  27658  nolesgn2o  28085  nolesgn2ores  28086  nogesgn1o  28087  nogesgn1ores  28088  noresle  28111  nosupprefixmo  28114  noinfprefixmo  28115  nosupres  28121  nosupbnd2lem1  28129  noinfres  28136  noinfbnd2lem1  28144  noetasuplem4  28150  noetainflem4  28154  addsval  28405  mulsval  28552  oniso  28714  addonbday  28722  bdayfinlem  28929  uhgrspansubgrlem  29928  wlkres  30306  redwlk  30308  pfxwlk  30323  subgrwlk  30326  cyclnumvtx  30445  foresf1o  33199  ofresid  33334  2ndresdju  33341  fdifsupp  33375  fdifsuppconst  33379  ressupprn  33380  fsuppcurry1  33412  fsuppcurry2  33413  mgcf1o  33663  gsumpart  33723  gsumhashmul  33727  tocyccntz  33804  isedom  33953  edomediv  33955  zzedom  33958  ply1edom  33959  edompidlem  33960  elrspunsn  34083  ressply10g  34202  evls1subd  34207  ply1gsumz  34234  evls1degle1  34239  evlextv  34285  esplyind  34318  vietalem  34322  dimkerim  34370  irngss  34430  rtelextdg2lem  34469  zarcmplem  34624  measres  34966  ftc2re  35338  reprsuc  35355  bnj1379  35571  noinfepregs  35942  fnlfvk3n0  36069  satom  36329  nmulprop  37154  bj-fvsnun1  38444  evlselv  43883  hashnna  46273  wessf1ornlem  46473  limcperiod  46913  limclner  46934  limsupresxr  47049  liminfresxr  47050  cncfperiod  47162  sssmf  48021  fcores  48410  isubgrgrim  49300  rhmsubcALTVlem2  49652  tposidres  50330  oppff1  50595  oppff1o  50596  fuco11  50779  opf11  50869  opf12  50870  fucoppclem  50873  oppfdiag1a  50881  lmddu  51181