Theorem fvresd 6860

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↾ cres 5633  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-res 5643  df-iota 6454  df-fv 6506

This theorem is referenced by:  fvressn  7116  fvsnun1  7137  fvsnun2  7138  fsnunfv  7142  resfvresima  7190  ovres  7533  resf1extb  7885  curry1  8054  curry2  8057  frrlem4  8239  frrlem12  8247  smores  8292  smores2  8294  tz7.44-2  8346  seqomlem1  8389  seqomlem4  8392  onasuc  8463  onmsuc  8464  onesuc  8465  ordtypelem4  9436  ordtypelem6  9438  ordtypelem7  9439  unxpwdom2  9503  cantnfres  9598  cantnfp1lem3  9601  ttrclss  9641  dfac12lem1  10066  ackbij2lem2  10161  cfsmolem  10192  ttukeylem3  10433  fpwwe2lem5  10558  fpwwe2lem8  10561  canthp1lem2  10576  addpqnq  10861  mulpqnq  10864  seqf1olem2  14004  seqcoll  14426  rlimres  15520  lo1res  15521  isercolllem3  15629  ackbijnn  15793  bitsf1  16415  sadcaddlem  16426  sadaddlem  16435  sadasslem  16439  sadeq  16441  eucalgcvga  16555  eucalg  16556  funcres  17863  1stf1  18158  2ndf1  18161  1stfcl  18163  2ndfcl  18164  prf1st  18170  prf2nd  18171  1st2ndprf  18172  uncf2  18203  diag12  18210  diag2  18211  curf2ndf  18213  yonedalem22  18244  lubval  18320  glbval  18333  gsumsplit1r  18655  resmhm  18788  resghm  19207  efgsres  19713  efgredlemd  19719  efgredlem  19722  dprdres  20005  dmdprdsplit2lem  20022  rhmsubclem2  20663  imadrhmcl  20774  abvres  20808  reslmhm  21047  psgndiflemB  21580  evls1addd  22336  evls1muld  22337  evls1vsca  22338  evls1fvcl  22340  evls1maprhm  22341  evls1maprnss  22343  cnpresti  23253  cnprest  23254  upxp  23588  uptx  23590  txkgen  23617  remetdval  24754  lmcau  25280  dvreslem  25876  dvres2lem  25877  dvlip2  25962  c1liplem1  25963  dvgt0lem1  25969  lhop1lem  25980  dvcnvrelem1  25984  dvcvx  25987  psercn  26391  efcvx  26414  reefgim  26415  resinf1o  26500  efif1olem4  26509  eff1olem  26512  eflog  26540  logcn  26611  loglesqrt  26725  asinrebnd  26865  jensen  26952  amgmlem  26953  lgamgulmlem2  26993  mpodvdsmulf1o  27157  dvdsmulf1o  27159  dchrabs  27223  sum2dchr  27237  nolesgn2o  27635  nolesgn2ores  27636  nogesgn1o  27637  nogesgn1ores  27638  noresle  27661  nosupprefixmo  27664  noinfprefixmo  27665  nosupres  27671  nosupbnd2lem1  27679  noinfres  27686  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  addsval  27954  mulsval  28101  oniso  28263  addonbday  28271  bdayfinlem  28478  uhgrspansubgrlem  29359  wlkres  29737  redwlk  29739  cyclnumvtx  29868  ofresid  32715  2ndresdju  32722  fdifsupp  32758  fdifsuppconst  32762  ressupprn  32763  fsuppcurry1  32797  fsuppcurry2  32798  mgcf1o  33063  gsumpart  33124  gsumhashmul  33128  tocyccntz  33205  elrspunsn  33489  ressply10g  33627  evls1subd  33632  ply1gsumz  33659  evlextv  33686  esplyind  33719  vietalem  33723  dimkerim  33771  irngss  33831  rtelextdg2lem  33870  zarcmplem  34025  measres  34366  ftc2re  34742  reprsuc  34759  bnj1379  34972  noinfepregs  35277  pfxwlk  35306  subgrwlk  35314  satom  35538  bj-fvsnun1  37569  selvvvval  43018  evlselv  43020  fnwe2lem3  43480  wessf1ornlem  45615  limcperiod  46058  limclner  46079  limsupresxr  46194  liminfresxr  46195  cncfperiod  46307  sssmf  47166  fcores  47515  isubgrgrim  48405  rhmsubcALTVlem2  48758  tposidres  49361  oppff1  49623  oppff1o  49624  fuco11  49801  opf11  49878  opf12  49879  fucoppclem  49882  oppfdiag1a  49890  lmddu  50142