MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvresd Structured version   Visualization version   GIF version

Theorem fvresd 6867
Description: The value of a restricted function, deduction version of fvres 6866. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypothesis
Ref Expression
fvresd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
fvresd (𝜑 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))

Proof of Theorem fvresd
StepHypRef Expression
1 fvresd.1 . 2 (𝜑𝐴𝐵)
2 fvres 6866 . 2 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
31, 2syl 17 1 (𝜑 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  cres 5640  cfv 6501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-res 5650  df-iota 6453  df-fv 6509
This theorem is referenced by:  fvressn  7113  fvsnun1  7133  fvsnun2  7134  fsnunfv  7138  resfvresima  7190  ovres  7525  curry1  8041  curry2  8044  frrlem4  8225  frrlem12  8233  smores  8303  smores2  8305  tz7.44-2  8358  seqomlem1  8401  seqomlem4  8404  onasuc  8479  onmsuc  8480  onesuc  8481  ordtypelem4  9464  ordtypelem6  9466  ordtypelem7  9467  unxpwdom2  9531  cantnfres  9620  cantnfp1lem3  9623  ttrclss  9663  dfac12lem1  10086  ackbij2lem2  10183  cfsmolem  10213  ttukeylem3  10454  fpwwe2lem5  10578  fpwwe2lem8  10581  canthp1lem2  10596  addpqnq  10881  mulpqnq  10884  seqf1olem2  13955  seqcoll  14370  rlimres  15447  lo1res  15448  isercolllem3  15558  ackbijnn  15720  bitsf1  16333  sadcaddlem  16344  sadaddlem  16353  sadasslem  16357  sadeq  16359  eucalgcvga  16469  eucalg  16470  funcres  17789  1stf1  18087  2ndf1  18090  1stfcl  18092  2ndfcl  18093  prf1st  18099  prf2nd  18100  1st2ndprf  18101  uncf2  18133  diag12  18140  diag2  18141  curf2ndf  18143  yonedalem22  18174  lubval  18252  glbval  18265  gsumsplit1r  18549  resmhm  18638  resghm  19031  efgsres  19527  efgredlemd  19533  efgredlem  19536  dprdres  19814  dmdprdsplit2lem  19831  abvres  20314  reslmhm  20529  psgndiflemB  21020  cnpresti  22655  cnprest  22656  upxp  22990  uptx  22992  txkgen  23019  remetdval  24168  lmcau  24693  dvreslem  25289  dvres2lem  25290  dvlip2  25375  c1liplem1  25376  dvgt0lem1  25382  lhop1lem  25393  dvcnvrelem1  25397  dvcvx  25400  psercn  25801  efcvx  25824  reefgim  25825  resinf1o  25908  efif1olem4  25917  eff1olem  25920  eflog  25948  logcn  26018  loglesqrt  26127  asinrebnd  26267  jensen  26354  amgmlem  26355  lgamgulmlem2  26395  dvdsmulf1o  26559  dchrabs  26624  sum2dchr  26638  nolesgn2o  27035  nolesgn2ores  27036  nogesgn1o  27037  nogesgn1ores  27038  noresle  27061  nosupprefixmo  27064  noinfprefixmo  27065  nosupres  27071  nosupbnd2lem1  27079  noinfres  27086  noinfbnd2lem1  27094  noetasuplem4  27100  noetainflem4  27104  addsval  27296  mulsval  27396  uhgrspansubgrlem  28280  wlkres  28660  redwlk  28662  ofresid  31600  2ndresdju  31607  fdifsuppconst  31646  ressupprn  31647  fsuppcurry1  31684  fsuppcurry2  31685  mgcf1o  31905  gsumpart  31939  gsumhashmul  31940  tocyccntz  32035  evls1addd  32313  evls1muld  32314  ressply10g  32317  dimkerim  32362  irngss  32401  evls1maprhm  32408  zarcmplem  32502  measres  32861  ftc2re  33251  reprsuc  33268  bnj1379  33482  pfxwlk  33757  subgrwlk  33766  satom  33990  bj-fvsnun1  35755  imadrhmcl  40745  fnwe2lem3  41408  wessf1ornlem  43477  limcperiod  43943  limclner  43966  limsupresxr  44081  liminfresxr  44082  cncfperiod  44194  sssmf  45053  fcores  45375  rhmsubclem2  46459  rhmsubcALTVlem2  46477
  Copyright terms: Public domain W3C validator