Theorem fvresd 6855

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↾ cres 5627  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-res 5637  df-iota 6449  df-fv 6501

This theorem is referenced by:  fvressn  7110  fvsnun1  7131  fvsnun2  7132  fsnunfv  7136  resfvresima  7184  ovres  7527  resf1extb  7879  curry1  8048  curry2  8051  frrlem4  8233  frrlem12  8241  smores  8286  smores2  8288  tz7.44-2  8340  seqomlem1  8383  seqomlem4  8386  onasuc  8457  onmsuc  8458  onesuc  8459  ordtypelem4  9430  ordtypelem6  9432  ordtypelem7  9433  unxpwdom2  9497  cantnfres  9592  cantnfp1lem3  9595  ttrclss  9635  dfac12lem1  10060  ackbij2lem2  10155  cfsmolem  10186  ttukeylem3  10427  fpwwe2lem5  10552  fpwwe2lem8  10555  canthp1lem2  10570  addpqnq  10855  mulpqnq  10858  seqf1olem2  13998  seqcoll  14420  rlimres  15514  lo1res  15515  isercolllem3  15623  ackbijnn  15787  bitsf1  16409  sadcaddlem  16420  sadaddlem  16429  sadasslem  16433  sadeq  16435  eucalgcvga  16549  eucalg  16550  funcres  17857  1stf1  18152  2ndf1  18155  1stfcl  18157  2ndfcl  18158  prf1st  18164  prf2nd  18165  1st2ndprf  18166  uncf2  18197  diag12  18204  diag2  18205  curf2ndf  18207  yonedalem22  18238  lubval  18314  glbval  18327  gsumsplit1r  18649  resmhm  18782  resghm  19201  efgsres  19707  efgredlemd  19713  efgredlem  19716  dprdres  19999  dmdprdsplit2lem  20016  rhmsubclem2  20657  imadrhmcl  20768  abvres  20802  reslmhm  21042  psgndiflemB  21593  evls1addd  22349  evls1muld  22350  evls1vsca  22351  evls1fvcl  22353  evls1maprhm  22354  evls1maprnss  22356  cnpresti  23266  cnprest  23267  upxp  23601  uptx  23603  txkgen  23630  remetdval  24767  lmcau  25293  dvreslem  25889  dvres2lem  25890  dvlip2  25975  c1liplem1  25976  dvgt0lem1  25982  lhop1lem  25993  dvcnvrelem1  25997  dvcvx  26000  psercn  26407  efcvx  26430  reefgim  26431  resinf1o  26516  efif1olem4  26525  eff1olem  26528  eflog  26556  logcn  26627  loglesqrt  26741  asinrebnd  26881  jensen  26969  amgmlem  26970  lgamgulmlem2  27010  mpodvdsmulf1o  27174  dvdsmulf1o  27176  dchrabs  27240  sum2dchr  27254  nolesgn2o  27652  nolesgn2ores  27653  nogesgn1o  27654  nogesgn1ores  27655  noresle  27678  nosupprefixmo  27681  noinfprefixmo  27682  nosupres  27688  nosupbnd2lem1  27696  noinfres  27703  noinfbnd2lem1  27711  noetasuplem4  27717  noetainflem4  27721  addsval  27971  mulsval  28118  oniso  28280  addonbday  28288  bdayfinlem  28495  uhgrspansubgrlem  29376  wlkres  29755  redwlk  29757  cyclnumvtx  29886  ofresid  32733  2ndresdju  32740  fdifsupp  32776  fdifsuppconst  32780  ressupprn  32781  fsuppcurry1  32815  fsuppcurry2  32816  mgcf1o  33081  gsumpart  33142  gsumhashmul  33146  tocyccntz  33223  elrspunsn  33507  ressply10g  33645  evls1subd  33650  ply1gsumz  33677  evlextv  33704  esplyind  33737  vietalem  33741  dimkerim  33790  irngss  33850  rtelextdg2lem  33889  zarcmplem  34044  measres  34385  ftc2re  34761  reprsuc  34778  bnj1379  34991  noinfepregs  35296  pfxwlk  35325  subgrwlk  35333  satom  35557  bj-fvsnun1  37588  selvvvval  43035  evlselv  43037  fnwe2lem3  43501  wessf1ornlem  45636  limcperiod  46079  limclner  46100  limsupresxr  46215  liminfresxr  46216  cncfperiod  46328  sssmf  47187  fcores  47530  isubgrgrim  48420  rhmsubcALTVlem2  48773  tposidres  49376  oppff1  49638  oppff1o  49639  fuco11  49816  opf11  49893  opf12  49894  fucoppclem  49897  oppfdiag1a  49905  lmddu  50157