Theorem fvresd 6684

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110   ↾ cres 5551  ‘cfv 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-xp 5555  df-res 5561  df-iota 6308  df-fv 6357

This theorem is referenced by:  fvressn  6918  fvsnun1  6938  fvsnun2  6939  fsnunfv  6943  resfvresima  6991  ovres  7308  curry1  7793  curry2  7796  smores  7983  smores2  7985  tz7.44-2  8037  seqomlem1  8080  seqomlem4  8083  onasuc  8147  onmsuc  8148  onesuc  8149  ordtypelem4  8979  ordtypelem6  8981  ordtypelem7  8982  unxpwdom2  9046  cantnfres  9134  cantnfp1lem3  9137  dfac12lem1  9563  ackbij2lem2  9656  cfsmolem  9686  ttukeylem3  9927  fpwwe2lem6  10051  fpwwe2lem9  10054  canthp1lem2  10069  addpqnq  10354  mulpqnq  10357  seqf1olem2  13404  seqcoll  13816  rlimres  14909  lo1res  14910  isercolllem3  15017  ackbijnn  15177  bitsf1  15789  sadcaddlem  15800  sadaddlem  15809  sadasslem  15813  sadeq  15815  eucalgcvga  15924  eucalg  15925  funcres  17160  1stf1  17436  2ndf1  17439  1stfcl  17441  2ndfcl  17442  prf1st  17448  prf2nd  17449  1st2ndprf  17450  uncf2  17481  diag12  17488  diag2  17489  curf2ndf  17491  yonedalem22  17522  lubval  17588  glbval  17601  gsumsplit1r  17891  resmhm  17979  resghm  18368  efgsres  18858  efgredlemd  18864  efgredlem  18867  dprdres  19144  dmdprdsplit2lem  19161  abvres  19604  reslmhm  19818  psgndiflemB  20738  cnpresti  21890  cnprest  21891  upxp  22225  uptx  22227  txkgen  22254  remetdval  23391  lmcau  23910  dvreslem  24501  dvres2lem  24502  dvlip2  24586  c1liplem1  24587  dvgt0lem1  24593  lhop1lem  24604  dvcnvrelem1  24608  dvcvx  24611  psercn  25008  efcvx  25031  reefgim  25032  resinf1o  25114  efif1olem4  25123  eff1olem  25126  eflog  25154  logcn  25224  loglesqrt  25333  asinrebnd  25473  jensen  25560  amgmlem  25561  lgamgulmlem2  25601  dvdsmulf1o  25765  dchrabs  25830  sum2dchr  25844  uhgrspansubgrlem  27066  wlkres  27446  redwlk  27448  ofresid  30383  fsuppcurry1  30455  fsuppcurry2  30456  tocyccntz  30781  dimkerim  31018  ftc2re  31864  reprsuc  31881  bnj1379  32097  pfxwlk  32365  subgrwlk  32374  satom  32598  frrlem4  33121  frrlem12  33129  nolesgn2o  33173  nolesgn2ores  33174  noresle  33195  noprefixmo  33197  nosupres  33202  nosupbnd2lem1  33210  noetalem3  33214  bj-fvsnun1  34531  fnwe2lem3  39645  wessf1ornlem  41438  limcperiod  41902  limclner  41925  limsupresxr  42040  liminfresxr  42041  cncfperiod  42155  sssmf  43009  rhmsubclem2  44352  rhmsubcALTVlem2  44370