MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvres Structured version   Unicode version

Theorem fvres 5870
Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fvres  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )

Proof of Theorem fvres
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 vex 3098 . . . . 5  |-  x  e. 
_V
21brres 5270 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 906 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5562 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5586 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5586 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2509 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804   class class class wbr 4437    |` cres 4991   iotacio 5539   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-xp 4995  df-res 5001  df-iota 5541  df-fv 5586
This theorem is referenced by:  funssfv  5871  fveqres  5890  feqresmpt  5912  dffv2  5931  fvreseq0  5972  respreima  6001  fveqressseq  6012  ffvresb  6047  fnressn  6068  fressnfv  6070  fvressn  6072  fvresi  6082  fvsnun1  6091  fvsnun2  6092  fsnunfv  6096  fnsuppresOLD  6116  funfvima  6132  funiunfv  6145  soisores  6208  isores3  6216  isoini2  6220  ovres  6427  ofres  6540  f1oweALT  6769  offres  6780  fo1stres  6809  fo2ndres  6810  curry1  6877  curry2  6880  fparlem1  6885  fparlem2  6886  fo2ndf  6892  f1o2ndf1  6893  fnsuppres  6929  smores  7025  smores2  7027  tfrlem1  7047  tz7.44-2  7075  fr0g  7103  frsuc  7104  tz7.48lem  7108  seqomlem1  7117  seqomlem2  7118  seqomlem3  7119  seqomlem4  7120  onasuc  7180  onmsuc  7181  onesuc  7182  resixp  7506  fofinf1o  7803  ixpfi2  7820  ordtypelem4  7949  ordtypelem6  7951  ordtypelem7  7952  unxpwdom2  8017  cantnfres  8099  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  dfac12lem1  8526  ackbij2lem2  8623  ackbij2lem3  8624  cfsmolem  8653  alephsing  8659  ttukeylem3  8894  fpwwe2lem6  9016  fpwwe2lem8  9018  fpwwe2lem9  9019  canthp1lem2  9034  inar1  9156  addpiord  9265  mulpiord  9266  addpqnq  9319  mulpqnq  9322  fseq1p1m1  11763  injresinj  11908  seqfeq2  12112  seqres  12116  seqf1olem2  12129  hashgval  12390  hashinf  12392  hashgval2  12428  hashf1lem1  12486  seqcoll  12494  swrdccat1  12664  shftidt  12897  rlimres  13363  lo1res  13364  climres  13380  isercolllem3  13471  fsumss  13529  isumclim3  13556  fsum2dlem  13567  ackbijnn  13622  fprodss  13737  fprod2dlem  13766  iprodclim3  13775  fprodefsum  13812  reeff1  13837  bitsf1  14078  sadcaddlem  14089  sadcadd  14090  sadadd2  14092  sadaddlem  14098  sadasslem  14102  sadeq  14104  eucalgcvga  14197  eucalg  14198  unbenlem  14408  strfv2d  14646  setsid  14655  setsnid  14656  funcres  15244  dmaf  15355  cdaf  15356  1stf1  15440  2ndf1  15443  1stfcl  15445  2ndfcl  15446  prf1st  15452  prf2nd  15453  1st2ndprf  15454  uncf2  15485  diag12  15492  diag2  15493  curf2ndf  15495  yonedalem22  15526  lubval  15593  glbval  15606  resmhm  15969  resghm  16262  efgsres  16735  efgredlemd  16741  efgredlem  16744  gsumzaddlem  16913  gsumzaddlemOLD  16915  dprdfadd  17039  dprdfaddOLD  17046  dprdres  17054  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  dprdcntz2  17065  dmdprdsplit2lem  17073  dprdsplit  17076  dpjidcl  17086  dpjidclOLD  17093  ablfac1eu  17103  mgpf  17189  prdscrngd  17241  abvres  17467  reslmhm  17677  ltbwe  18116  subrgascl  18142  subrgasclcl  18143  znf1o  18568  znunithash  18581  psgndiflemB  18614  smadiadetlem3  19148  cnpresti  19767  cnprest  19768  lmres  19779  tx1cn  20088  tx2cn  20089  upxp  20102  uptx  20104  ptrescn  20118  txkgen  20131  cnmpt1st  20147  cnmpt2nd  20148  ptuncnv  20286  ptunhmeo  20287  cnextfres  20546  prdstmdd  20600  prdsxmslem2  21010  subgnm2  21126  remetdval  21272  rescncf  21379  lmle  21718  lmcau  21729  ovoliunlem1  21891  ovolicc2lem4  21909  mblvol  21919  mbflimsup  22051  limcdif  22258  limcres  22268  dvreslem  22291  dvres2lem  22292  dvlip  22372  dvlipcn  22373  dvlip2  22374  c1liplem1  22375  c1lip1  22376  c1lip3  22378  dvgt0lem1  22381  dvivthlem1  22387  lhop1lem  22392  lhop  22395  dvcnvrelem1  22396  dvcvx  22399  ftc2ditglem  22424  itgsubstlem  22427  plyreres  22657  plyexmo  22687  aannenlem1  22702  taylthlem2  22747  ulmres  22761  ulmss  22770  psercn  22799  pserdvlem2  22801  reeff1o  22820  reefiso  22821  efcvx  22822  reefgim  22823  recosf1o  22900  resinf1o  22901  efif1olem4  22910  eff1olem  22913  relogcl  22941  eflog  22942  logef  22944  logeftb  22946  logltb  22962  logcn  23006  advlog  23013  advlogexp  23014  logtayl  23019  logccv  23022  dvcxp1  23094  cxpcn  23097  loglesqrt  23110  asinrebnd  23210  dvatan  23244  leibpi  23251  efrlim  23277  jensen  23296  amgmlem  23297  wilthlem3  23322  ftalem3  23326  dvdsmulf1o  23448  fsumdvdsmul  23449  dchrelbas2  23490  dchrabs  23513  sum2dchr  23527  dchrisumlem1  23652  logdivsum  23696  log2sumbnd  23707  ostth2  23800  ostth  23802  redwlk  24586  eupares  24953  ghsubgolemOLD  25350  sspnval  25628  hhssnv  26158  hhssmetdval  26172  foresf1o  27381  ofresid  27460  xpinpreima  27866  xpinpreima2  27867  cnre2csqlem  27870  rmulccn  27888  zzsnm  27919  zzsnmOLD  27920  cnzh  27929  rezh  27930  measres  28171  cntmeas  28175  cntnevol  28177  1stmbfm  28209  2ndmbfm  28210  eulerpartgbij  28289  eulerpartlemgvv  28293  eulerpartlemgs2  28297  iwrdsplit  28304  fibp1  28318  coinfliplem  28395  coinflipprob  28396  gsumnunsn  28471  plyrecld  28484  signstres  28510  lgamgulmlem2  28550  lgamcvg2  28575  subfacp1lem3  28604  subfacp1lem5  28606  erdszelem8  28620  txsconlem  28663  cvmfolem  28702  cvmliftmolem1  28704  cvmliftlem6  28713  cvmliftlem7  28714  cvmliftlem9  28716  mrsubff1  28852  msubff1  28894  fvresval  29173  dfrdg2  29204  wfrlem4  29322  frrlem4  29366  sltres  29400  nodense  29425  funpartfv  29571  bpolylem  29786  finixpnum  30014  itg2gt0cn  30046  dvcncxp1  30076  areacirclem2  30084  areacirclem4  30086  filnetlem4  30175  eqfnun  30188  sdclem2  30211  caures  30229  ismtyres  30280  imaiinfv  30601  mzpcompact2lem  30660  2rexfrabdioph  30705  3rexfrabdioph  30706  4rexfrabdioph  30707  6rexfrabdioph  30708  7rexfrabdioph  30709  jm2.27dlem1  30927  fnwe2lem2  30973  fnwe2lem3  30974  aomclem6  30981  deg1mhm  31143  hausgraph  31148  radcnvrat  31171  mccllem  31559  limcperiod  31588  limcleqr  31604  limclner  31611  resincncf  31631  cncfperiod  31635  icccncfext  31644  cncfiooicclem1  31650  dvbdfbdioolem1  31679  dvnprodlem1  31697  dvnprodlem2  31698  itgioocnicc  31730  stoweidlem28  31764  fourierdlem18  31861  fourierdlem40  31883  fourierdlem42  31885  fourierdlem46  31889  fourierdlem51  31894  fourierdlem70  31913  fourierdlem71  31914  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem78  31921  fourierdlem80  31923  fourierdlem81  31924  fourierdlem82  31925  fourierdlem84  31927  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem92  31935  fourierdlem93  31936  fourierdlem94  31937  fourierdlem101  31944  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  fourierdlem113  31956  afvres  32211  resmgmhm  32440  rhmsubclem2  32763  rhmsubcOLDlem2  32782  lincdifsn  32895  lindslinindimp2lem4  32932  lindslinindsimp2lem5  32933  lincresunit3lem2  32951  bnj1379  33757  bnj1253  33941  bnj1280  33944  diaintclN  36660  dibintclN  36769  dihintcl  36946
  Copyright terms: Public domain W3C validator