Theorem fvresd 6558

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

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081   ↾ cres 5445  ‘cfv 6225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-xp 5449  df-res 5455  df-iota 6189  df-fv 6233

This theorem is referenced by:  fvressn  6787  fvsnun1  6809  fvsnun2  6810  fsnunfv  6816  resfvresima  6862  ovres  7170  curry1  7655  curry2  7658  smores  7841  smores2  7843  tz7.44-2  7895  seqomlem1  7937  seqomlem4  7940  onasuc  8004  onmsuc  8005  onesuc  8006  ordtypelem4  8831  ordtypelem6  8833  ordtypelem7  8834  unxpwdom2  8898  cantnfres  8986  cantnfp1lem3  8989  dfac12lem1  9415  ackbij2lem2  9508  cfsmolem  9538  ttukeylem3  9779  fpwwe2lem6  9903  fpwwe2lem9  9906  canthp1lem2  9921  addpqnq  10206  mulpqnq  10209  seqf1olem2  13260  seqcoll  13670  rlimres  14749  lo1res  14750  isercolllem3  14857  ackbijnn  15016  bitsf1  15628  sadcaddlem  15639  sadaddlem  15648  sadasslem  15652  sadeq  15654  eucalgcvga  15759  eucalg  15760  funcres  16995  1stf1  17271  2ndf1  17274  1stfcl  17276  2ndfcl  17277  prf1st  17283  prf2nd  17284  1st2ndprf  17285  uncf2  17316  diag12  17323  diag2  17324  curf2ndf  17326  yonedalem22  17357  lubval  17423  glbval  17436  resmhm  17798  resghm  18115  efgsres  18591  efgredlemd  18597  efgredlem  18600  dprdres  18867  dmdprdsplit2lem  18884  abvres  19300  reslmhm  19514  psgndiflemB  20426  cnpresti  21580  cnprest  21581  upxp  21915  uptx  21917  txkgen  21944  remetdval  23080  lmcau  23599  dvreslem  24190  dvres2lem  24191  dvlip2  24275  c1liplem1  24276  dvgt0lem1  24282  lhop1lem  24293  dvcnvrelem1  24297  dvcvx  24300  psercn  24697  efcvx  24720  reefgim  24721  resinf1o  24801  efif1olem4  24810  eff1olem  24813  eflog  24841  logcn  24911  loglesqrt  25020  asinrebnd  25160  jensen  25248  amgmlem  25249  lgamgulmlem2  25289  dvdsmulf1o  25453  dchrabs  25518  sum2dchr  25532  uhgrspansubgrlem  26755  wlkres  27135  wlkresOLD  27137  redwlk  27139  ofresid  30079  fsuppcurry1  30149  fsuppcurry2  30150  tocyccntz  30423  dimkerim  30627  ftc2re  31486  reprsuc  31503  bnj1379  31719  subgrwlk  31987  satom  32211  frrlem4  32735  frrlem12  32743  nolesgn2o  32787  nolesgn2ores  32788  noresle  32809  noprefixmo  32811  nosupres  32816  nosupbnd2lem1  32824  noetalem3  32828  bj-fvsnun1  34095  fnwe2lem3  39137  wessf1ornlem  40985  limcperiod  41451  limclner  41474  limsupresxr  41589  liminfresxr  41590  cncfperiod  41703  sssmf  42557  rhmsubclem2  43836  rhmsubcALTVlem2  43854