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

Theorem fvres 5788
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 3037 . . . . 5  |-  x  e. 
_V
21brres 5192 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 904 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5481 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5504 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5504 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2448 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1826   class class class wbr 4367    |` cres 4915   iotacio 5458   ` cfv 5496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-xp 4919  df-res 4925  df-iota 5460  df-fv 5504
This theorem is referenced by:  funssfv  5789  fveqres  5808  feqresmpt  5828  dffv2  5847  fvreseq0  5889  respreima  5918  fveqressseq  5929  ffvresb  5964  fnressn  5985  fressnfv  5987  fvressn  5989  fvresi  5999  fvsnun1  6008  fvsnun2  6009  fsnunfv  6013  fnsuppresOLD  6033  funfvima  6048  funiunfv  6061  soisores  6124  isores3  6132  isoini2  6136  ovres  6341  ofres  6454  f1oweALT  6683  offres  6694  fo1stres  6723  fo2ndres  6724  curry1  6791  curry2  6794  fparlem1  6799  fparlem2  6800  fo2ndf  6806  f1o2ndf1  6807  fnsuppres  6845  smores  6941  smores2  6943  tfrlem1  6963  tz7.44-2  6991  fr0g  7019  frsuc  7020  tz7.48lem  7024  seqomlem1  7033  seqomlem2  7034  seqomlem3  7035  seqomlem4  7036  onasuc  7096  onmsuc  7097  onesuc  7098  resixp  7423  fofinf1o  7716  ixpfi2  7733  ordtypelem4  7861  ordtypelem6  7863  ordtypelem7  7864  unxpwdom2  7929  cantnfres  8009  cantnfp1lem3  8012  cantnfp1lem3OLD  8038  dfac12lem1  8436  ackbij2lem2  8533  ackbij2lem3  8534  cfsmolem  8563  alephsing  8569  ttukeylem3  8804  fpwwe2lem6  8924  fpwwe2lem8  8926  fpwwe2lem9  8927  canthp1lem2  8942  inar1  9064  addpiord  9173  mulpiord  9174  addpqnq  9227  mulpqnq  9230  fseq1p1m1  11674  injresinj  11825  seqfeq2  12033  seqres  12037  seqf1olem2  12050  hashgval  12310  hashinf  12312  hashgval2  12349  hashf1lem1  12408  seqcoll  12416  swrdccat1  12593  shftidt  12917  rlimres  13383  lo1res  13384  climres  13400  isercolllem3  13491  fsumss  13549  isumclim3  13576  fsum2dlem  13587  ackbijnn  13642  fprodss  13757  fprod2dlem  13786  iprodclim3  13795  fprodefsum  13832  reeff1  13857  bitsf1  14098  sadcaddlem  14109  sadcadd  14110  sadadd2  14112  sadaddlem  14118  sadasslem  14122  sadeq  14124  eucalgcvga  14217  eucalg  14218  unbenlem  14428  strfv2d  14668  setsid  14677  setsnid  14678  funcres  15302  dmaf  15445  cdaf  15446  1stf1  15578  2ndf1  15581  1stfcl  15583  2ndfcl  15584  prf1st  15590  prf2nd  15591  1st2ndprf  15592  uncf2  15623  diag12  15630  diag2  15631  curf2ndf  15633  yonedalem22  15664  lubval  15731  glbval  15744  resmhm  16107  resghm  16400  efgsres  16873  efgredlemd  16879  efgredlem  16882  gsumzaddlem  17051  gsumzaddlemOLD  17053  dprdfadd  17173  dprdfaddOLD  17180  dprdres  17188  dmdprdsplitlem  17197  dmdprdsplitlemOLD  17198  dprdcntz2  17199  dmdprdsplit2lem  17207  dprdsplit  17210  dpjidcl  17220  dpjidclOLD  17227  ablfac1eu  17237  mgpf  17323  prdscrngd  17375  abvres  17601  reslmhm  17811  ltbwe  18250  subrgascl  18276  subrgasclcl  18277  znf1o  18681  znunithash  18694  psgndiflemB  18727  smadiadetlem3  19255  cnpresti  19875  cnprest  19876  lmres  19887  tx1cn  20195  tx2cn  20196  upxp  20209  uptx  20211  ptrescn  20225  txkgen  20238  cnmpt1st  20254  cnmpt2nd  20255  ptuncnv  20393  ptunhmeo  20394  cnextfres  20653  prdstmdd  20707  prdsxmslem2  21117  subgnm2  21233  remetdval  21379  rescncf  21486  lmle  21825  lmcau  21836  ovoliunlem1  21998  ovolicc2lem4  22016  mblvol  22026  mbflimsup  22158  limcdif  22365  limcres  22375  dvreslem  22398  dvres2lem  22399  dvlip  22479  dvlipcn  22480  dvlip2  22481  c1liplem1  22482  c1lip1  22483  c1lip3  22485  dvgt0lem1  22488  dvivthlem1  22494  lhop1lem  22499  lhop  22502  dvcnvrelem1  22503  dvcvx  22506  ftc2ditglem  22531  itgsubstlem  22534  plyreres  22764  plyexmo  22794  aannenlem1  22809  taylthlem2  22854  ulmres  22868  ulmss  22877  psercn  22906  pserdvlem2  22908  reeff1o  22927  reefiso  22928  efcvx  22929  reefgim  22930  recosf1o  23007  resinf1o  23008  efif1olem4  23017  eff1olem  23020  relogcl  23048  eflog  23049  logef  23054  logeftb  23056  logltb  23072  logcn  23115  advlog  23122  advlogexp  23123  logtayl  23128  logccv  23131  dvcxp1  23203  cxpcn  23206  loglesqrt  23219  asinrebnd  23348  dvatan  23382  leibpi  23389  efrlim  23416  jensen  23435  amgmlem  23436  wilthlem3  23461  ftalem3  23465  dvdsmulf1o  23587  fsumdvdsmul  23588  dchrelbas2  23629  dchrabs  23652  sum2dchr  23666  dchrisumlem1  23791  logdivsum  23835  log2sumbnd  23846  ostth2  23939  ostth  23941  redwlk  24729  eupares  25096  ghsubgolemOLD  25489  sspnval  25767  hhssnv  26297  hhssmetdval  26311  foresf1o  27521  ofresid  27622  1stpreimas  27671  xpinpreima  28042  xpinpreima2  28043  cnre2csqlem  28046  rmulccn  28064  zzsnm  28095  cnzh  28104  rezh  28105  measres  28349  cntmeas  28353  cntnevol  28355  1stmbfm  28387  2ndmbfm  28388  carsggect  28445  omsmeas  28450  eulerpartgbij  28494  eulerpartlemgvv  28498  eulerpartlemgs2  28502  iwrdsplit  28509  fibp1  28523  coinfliplem  28600  coinflipprob  28601  gsumnunsn  28676  plyrecld  28689  signstres  28715  lgamgulmlem2  28761  lgamcvg2  28786  subfacp1lem3  28815  subfacp1lem5  28817  erdszelem8  28831  txsconlem  28874  cvmfolem  28913  cvmliftmolem1  28915  cvmliftlem6  28924  cvmliftlem7  28925  cvmliftlem9  28927  mrsubff1  29063  msubff1  29105  fvresval  29363  dfrdg2  29393  wfrlem4  29511  frrlem4  29555  sltres  29589  nodense  29614  funpartfv  29748  bpolylem  29963  finixpnum  30203  itg2gt0cn  30236  dvcncxp1  30266  areacirclem2  30274  areacirclem4  30276  filnetlem4  30365  eqfnun  30378  sdclem2  30401  caures  30419  ismtyres  30470  imaiinfv  30791  mzpcompact2lem  30849  2rexfrabdioph  30895  3rexfrabdioph  30896  4rexfrabdioph  30897  6rexfrabdioph  30898  7rexfrabdioph  30899  jm2.27dlem1  31117  fnwe2lem2  31163  fnwe2lem3  31164  aomclem6  31171  deg1mhm  31335  hausgraph  31340  radcnvrat  31363  mccllem  31771  limcperiod  31800  limcleqr  31816  limclner  31823  resincncf  31843  cncfperiod  31847  icccncfext  31856  cncfiooicclem1  31862  dvbdfbdioolem1  31891  dvnprodlem1  31909  dvnprodlem2  31910  itgioocnicc  31942  stoweidlem28  31976  fourierdlem18  32073  fourierdlem40  32095  fourierdlem42  32097  fourierdlem46  32101  fourierdlem51  32106  fourierdlem70  32125  fourierdlem71  32126  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem76  32131  fourierdlem78  32133  fourierdlem80  32135  fourierdlem81  32136  fourierdlem82  32137  fourierdlem84  32139  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem92  32147  fourierdlem93  32148  fourierdlem94  32149  fourierdlem101  32156  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem112  32167  fourierdlem113  32168  afvres  32423  pfxccat1  32585  resmgmhm  32804  rhmsubclem2  33095  rhmsubcALTVlem2  33114  lincdifsn  33225  lindslinindimp2lem4  33262  lindslinindsimp2lem5  33263  lincresunit3lem2  33281  fdivmpt  33361  bnj1379  34236  bnj1253  34420  bnj1280  34423  diaintclN  37198  dibintclN  37307  dihintcl  37484
  Copyright terms: Public domain W3C validator