Theorem fvresd 6881

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

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

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-res 5653  df-iota 6467  df-fv 6522

This theorem is referenced by:  fvressn  7137  fvsnun1  7159  fvsnun2  7160  fsnunfv  7164  resfvresima  7212  ovres  7558  resf1extb  7913  curry1  8086  curry2  8089  frrlem4  8271  frrlem12  8279  smores  8324  smores2  8326  tz7.44-2  8378  seqomlem1  8421  seqomlem4  8424  onasuc  8495  onmsuc  8496  onesuc  8497  ordtypelem4  9481  ordtypelem6  9483  ordtypelem7  9484  unxpwdom2  9548  cantnfres  9637  cantnfp1lem3  9640  ttrclss  9680  dfac12lem1  10104  ackbij2lem2  10199  cfsmolem  10230  ttukeylem3  10471  fpwwe2lem5  10595  fpwwe2lem8  10598  canthp1lem2  10613  addpqnq  10898  mulpqnq  10901  seqf1olem2  14014  seqcoll  14436  rlimres  15531  lo1res  15532  isercolllem3  15640  ackbijnn  15801  bitsf1  16423  sadcaddlem  16434  sadaddlem  16443  sadasslem  16447  sadeq  16449  eucalgcvga  16563  eucalg  16564  funcres  17865  1stf1  18160  2ndf1  18163  1stfcl  18165  2ndfcl  18166  prf1st  18172  prf2nd  18173  1st2ndprf  18174  uncf2  18205  diag12  18212  diag2  18213  curf2ndf  18215  yonedalem22  18246  lubval  18322  glbval  18335  gsumsplit1r  18621  resmhm  18754  resghm  19171  efgsres  19675  efgredlemd  19681  efgredlem  19684  dprdres  19967  dmdprdsplit2lem  19984  rhmsubclem2  20602  imadrhmcl  20713  abvres  20747  reslmhm  20966  psgndiflemB  21516  evls1addd  22265  evls1muld  22266  evls1vsca  22267  evls1fvcl  22269  evls1maprhm  22270  evls1maprnss  22272  cnpresti  23182  cnprest  23183  upxp  23517  uptx  23519  txkgen  23546  remetdval  24684  lmcau  25220  dvreslem  25817  dvres2lem  25818  dvlip2  25907  c1liplem1  25908  dvgt0lem1  25914  lhop1lem  25925  dvcnvrelem1  25929  dvcvx  25932  psercn  26343  efcvx  26366  reefgim  26367  resinf1o  26452  efif1olem4  26461  eff1olem  26464  eflog  26492  logcn  26563  loglesqrt  26678  asinrebnd  26818  jensen  26906  amgmlem  26907  lgamgulmlem2  26947  mpodvdsmulf1o  27111  dvdsmulf1o  27113  dchrabs  27178  sum2dchr  27192  nolesgn2o  27590  nolesgn2ores  27591  nogesgn1o  27592  nogesgn1ores  27593  noresle  27616  nosupprefixmo  27619  noinfprefixmo  27620  nosupres  27626  nosupbnd2lem1  27634  noinfres  27641  noinfbnd2lem1  27649  noetasuplem4  27655  noetainflem4  27659  addsval  27876  mulsval  28019  onsiso  28176  uhgrspansubgrlem  29224  wlkres  29605  redwlk  29607  cyclnumvtx  29737  ofresid  32573  2ndresdju  32580  fdifsupp  32615  fdifsuppconst  32619  ressupprn  32620  fsuppcurry1  32655  fsuppcurry2  32656  mgcf1o  32936  gsumpart  33004  gsumhashmul  33008  tocyccntz  33108  elrspunsn  33407  ressply10g  33543  evls1subd  33548  ply1gsumz  33571  dimkerim  33630  irngss  33689  rtelextdg2lem  33723  zarcmplem  33878  measres  34219  ftc2re  34596  reprsuc  34613  bnj1379  34827  pfxwlk  35118  subgrwlk  35126  satom  35350  bj-fvsnun1  37250  selvvvval  42580  evlselv  42582  fnwe2lem3  43048  wessf1ornlem  45186  limcperiod  45633  limclner  45656  limsupresxr  45771  liminfresxr  45772  cncfperiod  45884  sssmf  46743  fcores  47072  isubgrgrim  47933  rhmsubcALTVlem2  48274  tposidres  48878  oppff1  49141  oppff1o  49142  fuco11  49319  opf11  49396  opf12  49397  fucoppclem  49400  oppfdiag1a  49408  lmddu  49660