Theorem fvresd 6898

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↾ cres 5657  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-res 5667  df-iota 6489  df-fv 6541

This theorem is used by:  fvressn  7159  fvsnun1  7180  fvsnun2  7181  fsnunfv  7185  resfvresima  7234  ovres  7579  resf1extb  7931  curry1  8101  curry2  8104  frrlem4  8288  frrlem12  8296  smores  8341  smores2  8343  tz7.44-2  8396  seqomlem1  8439  seqomlem4  8442  onasuc  8515  onmsuc  8516  onesuc  8517  ordtypelem4  9493  ordtypelem6  9495  ordtypelem7  9496  unxpwdom2  9560  cantnfres  9656  cantnfp1lem3  9659  ttrclss  9699  dfac12lem1  10146  ackbij2lem2  10241  cfsmolem  10272  ttukeylem3  10513  fpwwe2lem5  10644  fpwwe2lem8  10647  canthp1lem2  10662  addpqnq  10947  mulpqnq  10950  seqf1olem2  14106  seqcoll  14529  rlimres  15645  lo1res  15646  isercolllem3  15754  ackbijnn  15917  bitsf1  16536  sadcaddlem  16547  sadaddlem  16556  sadasslem  16560  sadeq  16562  eucalgcvga  16676  eucalg  16677  funcres  17985  1stf1  18280  2ndf1  18283  1stfcl  18285  2ndfcl  18286  prf1st  18292  prf2nd  18293  1st2ndprf  18294  uncf2  18325  diag12  18332  diag2  18333  curf2ndf  18335  yonedalem22  18366  lubval  18442  glbval  18455  mgmn0plusgplusf  18742  gsumsplit1r  18789  resmhm  18929  resghm  19359  efgsres  19865  efgredlemd  19871  efgredlem  19874  dprdres  20157  dmdprdsplit2lem  20174  rhmsubclem2  20848  imadrhmcl  20963  abvres  20997  reslmhm  21236  psgndiflemB  21813  selvvvval  22358  evls1addd  22596  evls1muld  22597  evls1vsca  22598  evls1fvcl  22600  evls1maprhm  22601  evls1maprnss  22603  cnpresti  23513  cnprest  23514  upxp  23849  uptx  23851  txkgen  23878  remetdval  25015  lmcau  25541  dvreslem  26136  dvres2lem  26137  dvlip2  26222  c1liplem1  26223  dvgt0lem1  26229  lhop1lem  26240  dvcnvrelem1  26244  dvcvx  26247  psercn  26662  efcvx  26685  reefgim  26686  resinf1o  26773  efif1olem4  26782  eff1olem  26785  eflog  26813  logcn  26884  loglesqrt  26998  asinrebnd  27138  jensen  27225  amgmlem  27226  lgamgulmlem2  27266  mpodvdsmulf1o  27430  dvdsmulf1o  27432  dchrabs  27496  sum2dchr  27510  nolesgn2o  27907  nolesgn2ores  27908  nogesgn1o  27909  nogesgn1ores  27910  noresle  27933  nosupprefixmo  27936  noinfprefixmo  27937  nosupres  27943  nosupbnd2lem1  27951  noinfres  27958  noinfbnd2lem1  27966  noetasuplem4  27972  noetainflem4  27976  addsval  28227  mulsval  28374  oniso  28536  addonbday  28544  bdayfinlem  28751  uhgrspansubgrlem  29750  wlkres  30128  redwlk  30130  pfxwlk  30145  subgrwlk  30148  cyclnumvtx  30267  ofresid  33115  2ndresdju  33122  fdifsupp  33157  fdifsuppconst  33161  ressupprn  33162  fsuppcurry1  33195  fsuppcurry2  33196  mgcf1o  33443  gsumpart  33503  gsumhashmul  33507  tocyccntz  33584  elrspunsn  33857  ressply10g  33977  evls1subd  33982  ply1gsumz  34009  evlextv  34052  esplyind  34085  vietalem  34089  dimkerim  34137  irngss  34197  rtelextdg2lem  34236  zarcmplem  34391  measres  34733  ftc2re  35106  reprsuc  35123  bnj1379  35339  noinfepregs  35659  satom  35935  nmulprop  36770  bj-fvsnun1  38007  evlselv  43435  fnwe2lem3  43893  hashnna  45842  wessf1ornlem  46017  limcperiod  46458  limclner  46479  limsupresxr  46594  liminfresxr  46595  cncfperiod  46707  sssmf  47566  fcores  47955  isubgrgrim  48845  rhmsubcALTVlem2  49197  tposidres  49812  oppff1  50074  oppff1o  50075  fuco11  50252  opf11  50329  opf12  50330  fucoppclem  50333  oppfdiag1a  50341  lmddu  50593