Theorem fvresd 6842

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↾ cres 5621  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-res 5631  df-iota 6438  df-fv 6490

This theorem is referenced by:  fvressn  7096  fvsnun1  7118  fvsnun2  7119  fsnunfv  7123  resfvresima  7171  ovres  7515  resf1extb  7867  curry1  8037  curry2  8040  frrlem4  8222  frrlem12  8230  smores  8275  smores2  8277  tz7.44-2  8329  seqomlem1  8372  seqomlem4  8375  onasuc  8446  onmsuc  8447  onesuc  8448  ordtypelem4  9413  ordtypelem6  9415  ordtypelem7  9416  unxpwdom2  9480  cantnfres  9573  cantnfp1lem3  9576  ttrclss  9616  dfac12lem1  10038  ackbij2lem2  10133  cfsmolem  10164  ttukeylem3  10405  fpwwe2lem5  10529  fpwwe2lem8  10532  canthp1lem2  10547  addpqnq  10832  mulpqnq  10835  seqf1olem2  13949  seqcoll  14371  rlimres  15465  lo1res  15466  isercolllem3  15574  ackbijnn  15735  bitsf1  16357  sadcaddlem  16368  sadaddlem  16377  sadasslem  16381  sadeq  16383  eucalgcvga  16497  eucalg  16498  funcres  17803  1stf1  18098  2ndf1  18101  1stfcl  18103  2ndfcl  18104  prf1st  18110  prf2nd  18111  1st2ndprf  18112  uncf2  18143  diag12  18150  diag2  18151  curf2ndf  18153  yonedalem22  18184  lubval  18260  glbval  18273  gsumsplit1r  18561  resmhm  18694  resghm  19111  efgsres  19617  efgredlemd  19623  efgredlem  19626  dprdres  19909  dmdprdsplit2lem  19926  rhmsubclem2  20571  imadrhmcl  20682  abvres  20716  reslmhm  20956  psgndiflemB  21507  evls1addd  22256  evls1muld  22257  evls1vsca  22258  evls1fvcl  22260  evls1maprhm  22261  evls1maprnss  22263  cnpresti  23173  cnprest  23174  upxp  23508  uptx  23510  txkgen  23537  remetdval  24675  lmcau  25211  dvreslem  25808  dvres2lem  25809  dvlip2  25898  c1liplem1  25899  dvgt0lem1  25905  lhop1lem  25916  dvcnvrelem1  25920  dvcvx  25923  psercn  26334  efcvx  26357  reefgim  26358  resinf1o  26443  efif1olem4  26452  eff1olem  26455  eflog  26483  logcn  26554  loglesqrt  26669  asinrebnd  26809  jensen  26897  amgmlem  26898  lgamgulmlem2  26938  mpodvdsmulf1o  27102  dvdsmulf1o  27104  dchrabs  27169  sum2dchr  27183  nolesgn2o  27581  nolesgn2ores  27582  nogesgn1o  27583  nogesgn1ores  27584  noresle  27607  nosupprefixmo  27610  noinfprefixmo  27611  nosupres  27617  nosupbnd2lem1  27625  noinfres  27632  noinfbnd2lem1  27640  noetasuplem4  27646  noetainflem4  27650  addsval  27874  mulsval  28017  onsiso  28174  uhgrspansubgrlem  29235  wlkres  29614  redwlk  29616  cyclnumvtx  29745  ofresid  32585  2ndresdju  32592  fdifsupp  32627  fdifsuppconst  32631  ressupprn  32632  fsuppcurry1  32668  fsuppcurry2  32669  mgcf1o  32945  gsumpart  33010  gsumhashmul  33014  tocyccntz  33086  elrspunsn  33366  ressply10g  33502  evls1subd  33507  ply1gsumz  33531  dimkerim  33594  irngss  33654  rtelextdg2lem  33693  zarcmplem  33848  measres  34189  ftc2re  34566  reprsuc  34583  bnj1379  34797  pfxwlk  35097  subgrwlk  35105  satom  35329  bj-fvsnun1  37229  selvvvval  42558  evlselv  42560  fnwe2lem3  43025  wessf1ornlem  45163  limcperiod  45609  limclner  45632  limsupresxr  45747  liminfresxr  45748  cncfperiod  45860  sssmf  46719  fcores  47051  isubgrgrim  47913  rhmsubcALTVlem2  48266  tposidres  48870  oppff1  49133  oppff1o  49134  fuco11  49311  opf11  49388  opf12  49389  fucoppclem  49392  oppfdiag1a  49400  lmddu  49652