Theorem fvresd 6902

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   ↾ cres 5664  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-res 5674  df-iota 6493  df-fv 6545

This theorem is referenced by:  fvressn  7160  fvsnun1  7181  fvsnun2  7182  fsnunfv  7186  resfvresima  7234  ovres  7577  resf1extb  7930  curry1  8098  curry2  8101  frrlem4  8285  frrlem12  8293  smores  8338  smores2  8340  tz7.44-2  8393  seqomlem1  8436  seqomlem4  8439  onasuc  8512  onmsuc  8513  onesuc  8514  ordtypelem4  9482  ordtypelem6  9484  ordtypelem7  9485  unxpwdom2  9549  cantnfres  9645  cantnfp1lem3  9648  ttrclss  9688  dfac12lem1  10126  ackbij2lem2  10221  cfsmolem  10253  ttukeylem3  10494  fpwwe2lem5  10619  fpwwe2lem8  10622  canthp1lem2  10637  addpqnq  10922  mulpqnq  10925  seqf1olem2  14077  seqcoll  14500  rlimres  15608  lo1res  15609  isercolllem3  15717  ackbijnn  15881  bitsf1  16503  sadcaddlem  16514  sadaddlem  16523  sadasslem  16527  sadeq  16529  eucalgcvga  16643  eucalg  16644  funcres  17952  1stf1  18247  2ndf1  18250  1stfcl  18252  2ndfcl  18253  prf1st  18259  prf2nd  18260  1st2ndprf  18261  uncf2  18292  diag12  18299  diag2  18300  curf2ndf  18302  yonedalem22  18333  lubval  18409  glbval  18422  gsumsplit1r  18744  resmhm  18878  resghm  19301  efgsres  19807  efgredlemd  19813  efgredlem  19816  dprdres  20099  dmdprdsplit2lem  20116  rhmsubclem2  20770  imadrhmcl  20877  abvres  20911  reslmhm  21150  psgndiflemB  21718  selvvvval  22261  evls1addd  22499  evls1muld  22500  evls1vsca  22501  evls1fvcl  22503  evls1maprhm  22504  evls1maprnss  22506  cnpresti  23413  cnprest  23414  upxp  23748  uptx  23750  txkgen  23777  remetdval  24914  lmcau  25440  dvreslem  26036  dvres2lem  26037  dvlip2  26122  c1liplem1  26123  dvgt0lem1  26129  lhop1lem  26140  dvcnvrelem1  26144  dvcvx  26147  psercn  26554  efcvx  26577  reefgim  26578  resinf1o  26666  efif1olem4  26675  eff1olem  26678  eflog  26706  logcn  26777  loglesqrt  26891  asinrebnd  27031  jensen  27118  amgmlem  27119  lgamgulmlem2  27159  mpodvdsmulf1o  27323  dvdsmulf1o  27325  dchrabs  27389  sum2dchr  27403  nolesgn2o  27800  nolesgn2ores  27801  nogesgn1o  27802  nogesgn1ores  27803  noresle  27826  nosupprefixmo  27829  noinfprefixmo  27830  nosupres  27836  nosupbnd2lem1  27844  noinfres  27851  noinfbnd2lem1  27859  noetasuplem4  27865  noetainflem4  27869  addsval  28120  mulsval  28267  oniso  28429  addonbday  28437  bdayfinlem  28644  uhgrspansubgrlem  29580  wlkres  29958  redwlk  29960  cyclnumvtx  30089  ofresid  32927  2ndresdju  32934  fdifsupp  32970  fdifsuppconst  32974  ressupprn  32975  fsuppcurry1  33009  fsuppcurry2  33010  mgcf1o  33263  gsumpart  33323  gsumhashmul  33327  tocyccntz  33404  elrspunsn  33680  ressply10g  33801  evls1subd  33806  ply1gsumz  33833  evlextv  33876  esplyind  33909  vietalem  33913  dimkerim  33961  irngss  34021  rtelextdg2lem  34060  zarcmplem  34215  measres  34556  ftc2re  34929  reprsuc  34946  bnj1379  35162  noinfepregs  35468  pfxwlk  35514  subgrwlk  35522  satom  35746  nmulprop  36580  bj-fvsnun1  37786  evlselv  43212  fnwe2lem3  43670  hashnna  45619  wessf1ornlem  45794  limcperiod  46235  limclner  46256  limsupresxr  46371  liminfresxr  46372  cncfperiod  46484  sssmf  47343  fcores  47692  isubgrgrim  48582  rhmsubcALTVlem2  48935  tposidres  49548  oppff1  49810  oppff1o  49811  fuco11  49988  opf11  50065  opf12  50066  fucoppclem  50069  oppfdiag1a  50077  lmddu  50329