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

Theorem fvres 5803
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 3071 . . . . 5  |-  x  e. 
_V
21brres 5215 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 898 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5500 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5524 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5524 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2517 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   class class class wbr 4390    |` cres 4940   iotacio 5477   ` cfv 5516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-xp 4944  df-res 4950  df-iota 5479  df-fv 5524
This theorem is referenced by:  funssfv  5804  fveqres  5823  feqresmpt  5844  dffv2  5863  fvreseq0  5902  respreima  5931  ffvresb  5973  fnressn  5993  fressnfv  5995  fvresi  6003  fvunsn  6009  fvsnun1  6012  fvsnun2  6013  fsnunfv  6017  fnsuppresOLD  6037  funfvima  6051  funiunfv  6064  soisores  6117  isores3  6125  isoini2  6129  ovres  6330  ofres  6435  f1oweALT  6661  offres  6672  fo1stres  6700  fo2ndres  6701  curry1  6764  curry2  6767  fparlem1  6772  fparlem2  6773  fo2ndf  6779  f1o2ndf1  6780  fnsuppres  6816  smores  6913  smores2  6915  tfrlem1  6935  tz7.44-2  6963  fr0g  6991  frsuc  6992  tz7.48lem  6996  seqomlem1  7005  seqomlem2  7006  seqomlem3  7007  seqomlem4  7008  onasuc  7068  onmsuc  7069  onesuc  7070  resixp  7398  fofinf1o  7693  ixpfi2  7710  ordtypelem4  7836  ordtypelem6  7838  ordtypelem7  7839  unxpwdom2  7904  cantnfres  7986  cantnfp1lem3  7989  cantnfp1lem3OLD  8015  dfac12lem1  8413  ackbij2lem2  8510  ackbij2lem3  8511  cfsmolem  8540  alephsing  8546  ttukeylem3  8781  fpwwe2lem6  8903  fpwwe2lem8  8905  fpwwe2lem9  8906  canthp1lem2  8921  inar1  9043  addpiord  9154  mulpiord  9155  addpqnq  9208  mulpqnq  9211  fseq1p1m1  11635  injresinj  11740  seqfeq2  11930  seqres  11934  seqf1olem2  11947  hashgval  12207  hashinf  12209  hashgval2  12243  hashf1lem1  12310  seqcoll  12318  swrdccat1  12453  shftidt  12673  rlimres  13138  lo1res  13139  climres  13155  isercolllem3  13246  fsumss  13304  isumclim3  13328  fsum2dlem  13339  ackbijnn  13393  reeff1  13506  bitsf1  13744  sadcaddlem  13755  sadcadd  13756  sadadd2  13758  sadaddlem  13764  sadasslem  13768  sadeq  13770  eucalgcvga  13863  eucalg  13864  unbenlem  14071  strfv2d  14308  setsid  14317  setsnid  14318  funcres  14908  dmaf  15019  cdaf  15020  1stf1  15104  2ndf1  15107  1stfcl  15109  2ndfcl  15110  prf1st  15116  prf2nd  15117  1st2ndprf  15118  uncf2  15149  diag12  15156  diag2  15157  curf2ndf  15159  yonedalem22  15190  lubval  15256  glbval  15269  resmhm  15589  resghm  15865  efgsres  16339  efgredlemd  16345  efgredlem  16348  gsumzaddlem  16512  gsumzaddlemOLD  16514  dprdfadd  16615  dprdfaddOLD  16622  dprdres  16630  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dprdcntz2  16641  dmdprdsplit2lem  16649  dprdsplit  16652  dpjidcl  16662  dpjidclOLD  16669  ablfac1eu  16679  mgpf  16762  prdscrngd  16811  abvres  17030  reslmhm  17239  ltbwe  17661  subrgascl  17687  subrgasclcl  17688  znf1o  18093  znunithash  18106  psgndiflemB  18139  smadiadetlem3  18590  cnpresti  19008  cnprest  19009  lmres  19020  tx1cn  19298  tx2cn  19299  upxp  19312  uptx  19314  ptrescn  19328  txkgen  19341  cnmpt1st  19357  cnmpt2nd  19358  ptuncnv  19496  ptunhmeo  19497  cnextfres  19756  prdstmdd  19810  prdsxmslem2  20220  subgnm2  20336  remetdval  20482  rescncf  20589  lmle  20928  lmcau  20939  ovoliunlem1  21101  ovolicc2lem4  21119  mblvol  21129  mbflimsup  21260  limcdif  21467  limcres  21477  dvreslem  21500  dvres2lem  21501  dvlip  21581  dvlipcn  21582  dvlip2  21583  c1liplem1  21584  c1lip1  21585  c1lip3  21587  dvgt0lem1  21590  dvivthlem1  21596  lhop1lem  21601  lhop  21604  dvcnvrelem1  21605  dvcvx  21608  ftc2ditglem  21633  itgsubstlem  21636  plyreres  21865  plyexmo  21895  aannenlem1  21910  taylthlem2  21955  ulmres  21969  ulmss  21978  psercn  22007  pserdvlem2  22009  reeff1o  22028  reefiso  22029  efcvx  22030  reefgim  22031  recosf1o  22107  resinf1o  22108  efif1olem4  22117  eff1olem  22120  relogcl  22143  eflog  22144  logef  22146  logeftb  22148  logltb  22164  logcn  22208  advlog  22215  advlogexp  22216  logtayl  22221  logccv  22224  dvcxp1  22296  cxpcn  22299  loglesqr  22312  asinrebnd  22412  dvatan  22446  leibpi  22453  efrlim  22479  jensen  22498  amgmlem  22499  wilthlem3  22524  ftalem3  22528  dvdsmulf1o  22650  fsumdvdsmul  22651  dchrelbas2  22692  dchrabs  22715  sum2dchr  22729  dchrisumlem1  22854  logdivsum  22898  log2sumbnd  22909  ostth2  23002  ostth  23004  redwlk  23640  eupares  23731  ghsubgolem  23992  sspnval  24270  hhssnv  24800  hhssmetdval  24814  ofresid  26094  xpinpreima  26470  xpinpreima2  26471  cnre2csqlem  26474  rmulccn  26492  zzsnm  26523  zzsnmOLD  26524  cnzh  26533  rezh  26534  measres  26770  cntmeas  26774  cntnevol  26776  1stmbfm  26809  2ndmbfm  26810  eulerpartgbij  26889  eulerpartlemgvv  26893  eulerpartlemgs2  26897  iwrdsplit  26904  fibp1  26918  coinfliplem  26995  coinflipprob  26996  gsumnunsn  27071  plyrecld  27084  signstres  27110  lgamgulmlem2  27150  lgamcvg2  27175  subfacp1lem3  27204  subfacp1lem5  27206  erdszelem8  27220  txsconlem  27263  cvmfolem  27302  cvmliftmolem1  27304  cvmliftlem6  27313  cvmliftlem7  27314  cvmliftlem9  27316  fprodss  27595  fprodefsum  27619  fprod2dlem  27625  iprodclim3  27634  fvresval  27712  dfrdg2  27743  wfrlem4  27861  frrlem4  27905  sltres  27939  nodense  27964  funpartfv  28110  bpolylem  28325  finixpnum  28552  itg2gt0cn  28585  dvcncxp1  28615  areacirclem2  28623  areacirclem4  28625  filnetlem4  28740  eqfnun  28753  sdclem2  28776  caures  28794  ismtyres  28845  imaiinfv  29167  mzpcompact2lem  29226  2rexfrabdioph  29272  3rexfrabdioph  29273  4rexfrabdioph  29274  6rexfrabdioph  29275  7rexfrabdioph  29276  jm2.27dlem1  29496  fnwe2lem2  29542  fnwe2lem3  29543  aomclem6  29550  deg1mhm  29713  hausgraph  29718  stoweidlem28  29961  afvres  30216  fvressn  30290  lincdifsn  31065  lindslinindimp2lem4  31102  lindslinindsimp2lem5  31103  lincresunit3lem2  31121  m2cpminv  31222  bnj1379  32124  bnj1253  32308  bnj1280  32311  diaintclN  35009  dibintclN  35118  dihintcl  35295
  Copyright terms: Public domain W3C validator