Theorem fvresd 6911

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ↾ cres 5678  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-res 5688  df-iota 6495  df-fv 6551

This theorem is referenced by:  fvressn  7162  fvsnun1  7182  fvsnun2  7183  fsnunfv  7187  resfvresima  7239  ovres  7575  curry1  8092  curry2  8095  frrlem4  8276  frrlem12  8284  smores  8354  smores2  8356  tz7.44-2  8409  seqomlem1  8452  seqomlem4  8455  onasuc  8530  onmsuc  8531  onesuc  8532  ordtypelem4  9518  ordtypelem6  9520  ordtypelem7  9521  unxpwdom2  9585  cantnfres  9674  cantnfp1lem3  9677  ttrclss  9717  dfac12lem1  10140  ackbij2lem2  10237  cfsmolem  10267  ttukeylem3  10508  fpwwe2lem5  10632  fpwwe2lem8  10635  canthp1lem2  10650  addpqnq  10935  mulpqnq  10938  seqf1olem2  14012  seqcoll  14429  rlimres  15506  lo1res  15507  isercolllem3  15617  ackbijnn  15778  bitsf1  16391  sadcaddlem  16402  sadaddlem  16411  sadasslem  16415  sadeq  16417  eucalgcvga  16527  eucalg  16528  funcres  17850  1stf1  18148  2ndf1  18151  1stfcl  18153  2ndfcl  18154  prf1st  18160  prf2nd  18161  1st2ndprf  18162  uncf2  18194  diag12  18201  diag2  18202  curf2ndf  18204  yonedalem22  18235  lubval  18313  glbval  18326  gsumsplit1r  18612  resmhm  18737  resghm  19146  efgsres  19647  efgredlemd  19653  efgredlem  19656  dprdres  19939  dmdprdsplit2lem  19956  imadrhmcl  20556  abvres  20590  reslmhm  20807  psgndiflemB  21372  cnpresti  23012  cnprest  23013  upxp  23347  uptx  23349  txkgen  23376  remetdval  24525  lmcau  25054  dvreslem  25650  dvres2lem  25651  dvlip2  25736  c1liplem1  25737  dvgt0lem1  25743  lhop1lem  25754  dvcnvrelem1  25758  dvcvx  25761  psercn  26162  efcvx  26185  reefgim  26186  resinf1o  26269  efif1olem4  26278  eff1olem  26281  eflog  26309  logcn  26379  loglesqrt  26490  asinrebnd  26630  jensen  26717  amgmlem  26718  lgamgulmlem2  26758  dvdsmulf1o  26922  dchrabs  26987  sum2dchr  27001  nolesgn2o  27398  nolesgn2ores  27399  nogesgn1o  27400  nogesgn1ores  27401  noresle  27424  nosupprefixmo  27427  noinfprefixmo  27428  nosupres  27434  nosupbnd2lem1  27442  noinfres  27449  noinfbnd2lem1  27457  noetasuplem4  27463  noetainflem4  27467  addsval  27672  mulsval  27792  uhgrspansubgrlem  28802  wlkres  29182  redwlk  29184  ofresid  32122  2ndresdju  32129  fdifsuppconst  32166  ressupprn  32167  fsuppcurry1  32205  fsuppcurry2  32206  mgcf1o  32428  gsumpart  32465  gsumhashmul  32466  tocyccntz  32561  elrspunsn  32809  evls1addd  32910  evls1muld  32911  evls1vsca  32912  ressply10g  32918  ply1gsumz  32932  dimkerim  32988  irngss  33028  evls1fvcl  33035  evls1maprhm  33036  evls1maprnss  33038  zarcmplem  33147  measres  33506  ftc2re  33896  reprsuc  33913  bnj1379  34127  pfxwlk  34400  subgrwlk  34409  satom  34633  bj-fvsnun1  36439  selvvvval  41459  evlselv  41461  fnwe2lem3  42096  wessf1ornlem  44183  limcperiod  44643  limclner  44666  limsupresxr  44781  liminfresxr  44782  cncfperiod  44894  sssmf  45753  fcores  46076  rhmsubclem2  47074  rhmsubcALTVlem2  47092