Theorem fvresd 6905

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ↾ cres 5665  ‘cfv 6540

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-res 5675  df-iota 6496  df-fv 6548

This theorem is used by:  fvressn  7165  fvsnun1  7186  fvsnun2  7187  fsnunfv  7191  resfvresima  7240  ovres  7585  resf1extb  7937  curry1  8105  curry2  8108  frrlem4  8292  frrlem12  8300  smores  8345  smores2  8347  tz7.44-2  8400  seqomlem1  8443  seqomlem4  8446  onasuc  8519  onmsuc  8520  onesuc  8521  ordtypelem4  9490  ordtypelem6  9492  ordtypelem7  9493  unxpwdom2  9557  cantnfres  9653  cantnfp1lem3  9656  ttrclss  9696  dfac12lem1  10143  ackbij2lem2  10238  cfsmolem  10269  ttukeylem3  10510  fpwwe2lem5  10635  fpwwe2lem8  10638  canthp1lem2  10653  addpqnq  10938  mulpqnq  10941  seqf1olem2  14096  seqcoll  14519  rlimres  15633  lo1res  15634  isercolllem3  15742  ackbijnn  15905  bitsf1  16526  sadcaddlem  16537  sadaddlem  16546  sadasslem  16550  sadeq  16552  eucalgcvga  16666  eucalg  16667  funcres  17975  1stf1  18270  2ndf1  18273  1stfcl  18275  2ndfcl  18276  prf1st  18282  prf2nd  18283  1st2ndprf  18284  uncf2  18315  diag12  18322  diag2  18323  curf2ndf  18325  yonedalem22  18356  lubval  18432  glbval  18445  mgmn0plusgplusf  18732  gsumsplit1r  18777  resmhm  18916  resghm  19346  efgsres  19852  efgredlemd  19858  efgredlem  19861  dprdres  20144  dmdprdsplit2lem  20161  rhmsubclem2  20835  imadrhmcl  20950  abvres  20984  reslmhm  21223  psgndiflemB  21800  selvvvval  22343  evls1addd  22581  evls1muld  22582  evls1vsca  22583  evls1fvcl  22585  evls1maprhm  22586  evls1maprnss  22588  cnpresti  23495  cnprest  23496  upxp  23831  uptx  23833  txkgen  23860  remetdval  24997  lmcau  25523  dvreslem  26119  dvres2lem  26120  dvlip2  26205  c1liplem1  26206  dvgt0lem1  26212  lhop1lem  26223  dvcnvrelem1  26227  dvcvx  26230  psercn  26640  efcvx  26663  reefgim  26664  resinf1o  26752  efif1olem4  26761  eff1olem  26764  eflog  26792  logcn  26863  loglesqrt  26977  asinrebnd  27117  jensen  27204  amgmlem  27205  lgamgulmlem2  27245  mpodvdsmulf1o  27409  dvdsmulf1o  27411  dchrabs  27475  sum2dchr  27489  nolesgn2o  27886  nolesgn2ores  27887  nogesgn1o  27888  nogesgn1ores  27889  noresle  27912  nosupprefixmo  27915  noinfprefixmo  27916  nosupres  27922  nosupbnd2lem1  27930  noinfres  27937  noinfbnd2lem1  27945  noetasuplem4  27951  noetainflem4  27955  addsval  28206  mulsval  28353  oniso  28515  addonbday  28523  bdayfinlem  28730  uhgrspansubgrlem  29698  wlkres  30076  redwlk  30078  pfxwlk  30093  subgrwlk  30096  cyclnumvtx  30215  ofresid  33058  2ndresdju  33065  fdifsupp  33101  fdifsuppconst  33105  ressupprn  33106  fsuppcurry1  33139  fsuppcurry2  33140  mgcf1o  33387  gsumpart  33447  gsumhashmul  33451  tocyccntz  33528  elrspunsn  33801  ressply10g  33921  evls1subd  33926  ply1gsumz  33953  evlextv  33996  esplyind  34029  vietalem  34033  dimkerim  34081  irngss  34141  rtelextdg2lem  34180  zarcmplem  34335  measres  34677  ftc2re  35050  reprsuc  35067  bnj1379  35283  noinfepregs  35603  satom  35885  nmulprop  36719  bj-fvsnun1  37956  evlselv  43379  fnwe2lem3  43837  hashnna  45786  wessf1ornlem  45961  limcperiod  46402  limclner  46423  limsupresxr  46538  liminfresxr  46539  cncfperiod  46651  sssmf  47510  fcores  47862  isubgrgrim  48752  rhmsubcALTVlem2  49104  tposidres  49721  oppff1  49983  oppff1o  49984  fuco11  50161  opf11  50238  opf12  50239  fucoppclem  50242  oppfdiag1a  50250  lmddu  50502