Theorem fvresd 6903

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↾ cres 5653  ‘cfv 6537

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-res 5663  df-iota 6493  df-fv 6545

This theorem is used by:  fvressn  7164  fvsnun1  7185  fvsnun2  7186  fsnunfv  7190  resfvresima  7239  ovres  7584  resf1extb  7944  curry1  8113  curry2  8116  frrlem4  8300  frrlem12  8308  smores  8353  smores2  8355  tz7.44-2  8408  seqomlem1  8453  seqomlem4  8456  onasuc  8529  onmsuc  8530  onesuc  8531  ordtypelem4  9508  ordtypelem6  9510  ordtypelem7  9511  unxpwdom2  9575  cantnfres  9671  cantnfp1lem3  9674  ttrclss  9714  dfac12lem1  10215  ackbij2lem2  10310  cfsmolem  10341  ttukeylem3  10582  fpwwe2lem5  10713  fpwwe2lem8  10716  canthp1lem2  10731  addpqnq  11016  mulpqnq  11019  seqf1olem2  14178  seqcoll  14602  rlimres  15718  lo1res  15719  isercolllem3  15827  ackbijnn  15990  bitsf1  16609  sadcaddlem  16620  sadaddlem  16629  sadasslem  16633  sadeq  16635  eucalgcvga  16754  eucalg  16755  funcres  18064  1stf1  18359  2ndf1  18362  1stfcl  18364  2ndfcl  18365  prf1st  18371  prf2nd  18372  1st2ndprf  18373  uncf2  18404  diag12  18411  diag2  18412  curf2ndf  18414  yonedalem22  18445  lubval  18521  glbval  18534  mgmn0plusgplusf  18821  gsumsplit1r  18869  resmhm  19009  resghm  19439  efgsres  19945  efgredlemd  19951  efgredlem  19954  dprdres  20237  dmdprdsplit2lem  20254  rhmsubclem2  20931  imadrhmcl  21047  abvres  21081  reslmhm  21320  psgndiflemB  21899  selvvvval  22444  evls1addd  22682  evls1muld  22683  evls1vsca  22684  evls1fvcl  22686  evls1maprhm  22687  evls1maprnss  22689  cnpresti  23599  cnprest  23600  upxp  23935  uptx  23937  txkgen  23964  remetdval  25101  lmcau  25627  dvreslem  26222  dvres2lem  26223  dvlip2  26308  c1liplem1  26309  dvgt0lem1  26315  lhop1lem  26326  dvcnvrelem1  26330  dvcvx  26333  psercn  26746  efcvx  26769  reefgim  26770  resinf1o  26857  efif1olem4  26866  eff1olem  26869  eflog  26897  logcn  26968  loglesqrt  27082  asinrebnd  27222  jensen  27309  amgmlem  27310  lgamgulmlem2  27350  mpodvdsmulf1o  27514  dvdsmulf1o  27516  dchrabs  27580  sum2dchr  27594  nolesgn2o  28021  nolesgn2ores  28022  nogesgn1o  28023  nogesgn1ores  28024  noresle  28047  nosupprefixmo  28050  noinfprefixmo  28051  nosupres  28057  nosupbnd2lem1  28065  noinfres  28072  noinfbnd2lem1  28080  noetasuplem4  28086  noetainflem4  28090  addsval  28341  mulsval  28488  oniso  28650  addonbday  28658  bdayfinlem  28865  uhgrspansubgrlem  29864  wlkres  30242  redwlk  30244  pfxwlk  30259  subgrwlk  30262  cyclnumvtx  30381  ofresid  33229  2ndresdju  33236  fdifsupp  33271  fdifsuppconst  33275  ressupprn  33276  fsuppcurry1  33309  fsuppcurry2  33310  mgcf1o  33557  gsumpart  33617  gsumhashmul  33621  tocyccntz  33698  elrspunsn  33972  ressply10g  34092  evls1subd  34097  ply1gsumz  34124  evlextv  34167  esplyind  34200  vietalem  34204  dimkerim  34252  irngss  34312  rtelextdg2lem  34351  zarcmplem  34506  measres  34848  ftc2re  35220  reprsuc  35237  bnj1379  35453  noinfepregs  35784  satom  36100  nmulprop  36919  bj-fvsnun1  38156  evlselv  43597  fnwe2lem3  44038  hashnna  45987  wessf1ornlem  46169  limcperiod  46609  limclner  46630  limsupresxr  46745  liminfresxr  46746  cncfperiod  46858  sssmf  47717  fcores  48106  isubgrgrim  48996  rhmsubcALTVlem2  49348  tposidres  49963  oppff1  50225  oppff1o  50226  fuco11  50403  opf11  50480  opf12  50481  fucoppclem  50484  oppfdiag1a  50492  lmddu  50744