Theorem fvresd 6901

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ↾ cres 5663  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-res 5673  df-iota 6492  df-fv 6544

This theorem is referenced by:  fvressn  7159  fvsnun1  7180  fvsnun2  7181  fsnunfv  7185  resfvresima  7233  ovres  7576  resf1extb  7927  curry1  8095  curry2  8098  frrlem4  8282  frrlem12  8290  smores  8335  smores2  8337  tz7.44-2  8390  seqomlem1  8433  seqomlem4  8436  onasuc  8509  onmsuc  8510  onesuc  8511  ordtypelem4  9479  ordtypelem6  9481  ordtypelem7  9482  unxpwdom2  9546  cantnfres  9642  cantnfp1lem3  9645  ttrclss  9685  dfac12lem1  10123  ackbij2lem2  10218  cfsmolem  10249  ttukeylem3  10490  fpwwe2lem5  10615  fpwwe2lem8  10618  canthp1lem2  10633  addpqnq  10918  mulpqnq  10921  seqf1olem2  14074  seqcoll  14497  rlimres  15605  lo1res  15606  isercolllem3  15714  ackbijnn  15878  bitsf1  16499  sadcaddlem  16510  sadaddlem  16519  sadasslem  16523  sadeq  16525  eucalgcvga  16639  eucalg  16640  funcres  17948  1stf1  18243  2ndf1  18246  1stfcl  18248  2ndfcl  18249  prf1st  18255  prf2nd  18256  1st2ndprf  18257  uncf2  18288  diag12  18295  diag2  18296  curf2ndf  18298  yonedalem22  18329  lubval  18405  glbval  18418  gsumsplit1r  18740  resmhm  18874  resghm  19297  efgsres  19803  efgredlemd  19809  efgredlem  19812  dprdres  20095  dmdprdsplit2lem  20112  rhmsubclem2  20785  imadrhmcl  20900  abvres  20934  reslmhm  21173  psgndiflemB  21750  selvvvval  22293  evls1addd  22531  evls1muld  22532  evls1vsca  22533  evls1fvcl  22535  evls1maprhm  22536  evls1maprnss  22538  cnpresti  23445  cnprest  23446  upxp  23780  uptx  23782  txkgen  23809  remetdval  24946  lmcau  25472  dvreslem  26068  dvres2lem  26069  dvlip2  26154  c1liplem1  26155  dvgt0lem1  26161  lhop1lem  26172  dvcnvrelem1  26176  dvcvx  26179  psercn  26589  efcvx  26612  reefgim  26613  resinf1o  26701  efif1olem4  26710  eff1olem  26713  eflog  26741  logcn  26812  loglesqrt  26926  asinrebnd  27066  jensen  27153  amgmlem  27154  lgamgulmlem2  27194  mpodvdsmulf1o  27358  dvdsmulf1o  27360  dchrabs  27424  sum2dchr  27438  nolesgn2o  27835  nolesgn2ores  27836  nogesgn1o  27837  nogesgn1ores  27838  noresle  27861  nosupprefixmo  27864  noinfprefixmo  27865  nosupres  27871  nosupbnd2lem1  27879  noinfres  27886  noinfbnd2lem1  27894  noetasuplem4  27900  noetainflem4  27904  addsval  28155  mulsval  28302  oniso  28464  addonbday  28472  bdayfinlem  28679  uhgrspansubgrlem  29640  wlkres  30018  redwlk  30020  cyclnumvtx  30149  ofresid  32987  2ndresdju  32994  fdifsupp  33030  fdifsuppconst  33034  ressupprn  33035  fsuppcurry1  33069  fsuppcurry2  33070  mgcf1o  33323  gsumpart  33383  gsumhashmul  33387  tocyccntz  33464  elrspunsn  33737  ressply10g  33857  evls1subd  33862  ply1gsumz  33889  evlextv  33932  esplyind  33965  vietalem  33969  dimkerim  34017  irngss  34077  rtelextdg2lem  34116  zarcmplem  34271  measres  34612  ftc2re  34985  reprsuc  35002  bnj1379  35218  noinfepregs  35546  pfxwlk  35616  subgrwlk  35624  satom  35848  nmulprop  36682  bj-fvsnun1  37899  evlselv  43321  fnwe2lem3  43779  hashnna  45728  wessf1ornlem  45903  limcperiod  46344  limclner  46365  limsupresxr  46480  liminfresxr  46481  cncfperiod  46593  sssmf  47452  fcores  47804  isubgrgrim  48694  rhmsubcALTVlem2  49047  tposidres  49664  oppff1  49926  oppff1o  49927  fuco11  50104  opf11  50181  opf12  50182  fucoppclem  50185  oppfdiag1a  50193  lmddu  50445