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

Theorem fvres 5558
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 2804 . . . . 5  |-  x  e. 
_V
21brres 4977 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 873 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5256 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5279 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5279 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2353 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   class class class wbr 4039    |` cres 4707   iotacio 5233   ` cfv 5271
This theorem is referenced by:  funssfv  5559  fveqres  5576  feqresmpt  5592  dffv2  5608  fvreseq  5644  respreima  5670  ffvresb  5706  fnressn  5721  fressnfv  5723  fvresi  5727  fvunsn  5728  fvsnun1  5731  fvsnun2  5732  fsnunfv  5736  fnsuppres  5748  funfvima  5769  funiunfv  5790  soisores  5840  isores3  5848  isoini2  5852  f1oweALT  5867  ovres  6003  offres  6108  ofres  6110  fo1stres  6159  fo2ndres  6160  curry1  6226  curry2  6229  fparlem1  6234  fparlem2  6235  smores  6385  smores2  6387  tfrlem5  6412  tz7.44-2  6436  fr0g  6464  frsuc  6465  tz7.48lem  6469  seqomlem1  6478  seqomlem2  6479  seqomlem3  6480  seqomlem4  6481  onasuc  6543  onmsuc  6544  onesuc  6545  resixp  6867  fofinf1o  7153  ixpfi2  7170  ordtypelem4  7252  ordtypelem6  7254  ordtypelem7  7255  unxpwdom2  7318  cantnfres  7395  cantnfp1lem3  7398  dfac12lem1  7785  ackbij2lem2  7882  ackbij2lem3  7883  cfsmolem  7912  alephsing  7918  ttukeylem3  8154  fpwwe2lem6  8273  fpwwe2lem8  8275  fpwwe2lem9  8276  canthp1lem2  8291  inar1  8413  addpiord  8524  mulpiord  8525  addpqnq  8578  mulpqnq  8581  fseq1p1m1  10873  seqfeq2  11085  seqres  11089  seqf1olem2  11102  hashgval  11356  hashinf  11358  hashgval2  11376  hashf1lem1  11409  seqcoll  11417  swrdccat1  11476  shftidt  11593  rlimres  12048  lo1res  12049  climres  12065  isercolllem3  12156  fsumss  12214  isumclim3  12238  fsum2dlem  12249  ackbijnn  12302  reeff1  12416  bitsf1  12653  sadcaddlem  12664  sadcadd  12665  sadadd2  12667  sadaddlem  12673  sadasslem  12677  sadeq  12679  eucalgcvga  12772  eucalg  12773  unbenlem  12971  strfv2d  13194  setsid  13203  setsnid  13204  funcres  13786  dmaf  13897  cdaf  13898  1stf1  13982  2ndf1  13985  1stfcl  13987  2ndfcl  13988  prf1st  13994  prf2nd  13995  1st2ndprf  13996  uncf2  14027  diag12  14034  diag2  14035  curf2ndf  14037  yonedalem22  14068  resmhm  14452  resghm  14715  efgsres  15063  efgredlemd  15069  efgredlem  15072  gsumzaddlem  15219  dprdfadd  15271  dprdres  15279  dmdprdsplitlem  15288  dprdcntz2  15289  dmdprdsplit2lem  15296  dprdsplit  15299  dpjidcl  15309  ablfac1eu  15324  mgpf  15368  prdscrngd  15412  abvres  15620  reslmhm  15825  ltbwe  16230  subrgascl  16255  subrgasclcl  16256  znf1o  16521  znunithash  16534  cnpresti  17032  cnprest  17033  lmres  17044  tx1cn  17319  tx2cn  17320  upxp  17333  uptx  17335  ptrescn  17349  txkgen  17362  cnmpt1st  17378  cnmpt2nd  17379  ptuncnv  17514  ptunhmeo  17515  prdstmdd  17822  prdsxmslem2  18091  subgnm2  18166  remetdval  18311  rescncf  18417  lmle  18743  lmcau  18754  ovoliunlem1  18877  ovolicc2lem4  18895  mblvol  18905  mbflimsup  19037  limcdif  19242  limcres  19252  dvreslem  19275  dvres2lem  19276  dvlip  19356  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  c1lip1  19360  c1lip3  19362  dvgt0lem1  19365  dvivthlem1  19371  lhop1lem  19376  lhop  19379  dvcnvrelem1  19380  dvcvx  19383  ftc2ditglem  19408  itgsubstlem  19411  plyreres  19679  plyexmo  19709  aannenlem1  19724  taylthlem2  19769  ulmres  19783  ulmss  19790  psercn  19818  pserdvlem2  19820  reeff1o  19839  reefiso  19840  efcvx  19841  reefgim  19842  recosf1o  19913  resinf1o  19914  efif1olem4  19923  eff1olem  19926  relogcl  19948  eflog  19949  logef  19951  logeftb  19953  logltb  19969  logcn  20010  advlog  20017  advlogexp  20018  logtayl  20023  logccv  20026  dvcxp1  20098  cxpcn  20101  loglesqr  20114  asinrebnd  20213  dvatan  20247  leibpi  20254  efrlim  20280  jensen  20299  amgmlem  20300  wilthlem3  20324  ftalem3  20328  dvdsmulf1o  20450  fsumdvdsmul  20451  dchrelbas2  20492  dchrabs  20515  sum2dchr  20529  dchrisumlem1  20654  logdivsum  20698  log2sumbnd  20709  ostth2  20802  ostth  20804  ghsubgolem  21053  sspnval  21329  hhssnv  21857  hhssmetdval  21871  cntnevol  23191  xpinpreima  23305  xpinpreima2  23306  cnre2csqlem  23309  rmulccn  23316  measres  23564  cntmeas  23568  1stmbfm  23580  2ndmbfm  23581  coinfliplem  23694  coinflipprob  23695  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem8  23744  txsconlem  23786  cvmfolem  23825  cvmliftmolem1  23827  cvmliftlem6  23836  cvmliftlem7  23837  cvmliftlem9  23839  eupares  23914  fvresval  24194  dfrdg2  24223  wfrlem4  24330  frrlem4  24355  sltres  24389  nodense  24414  funpartfv  24555  bpolylem  24855  itg2gt0cn  25006  areacirclem4  25030  areacirclem5  25032  oprssopvg  25137  eqfnung2  25221  prl2  25272  idsubfun  25961  vtare  25988  vtarsu  25989  vtarl  25990  filnetlem4  26433  eqfnun  26490  sdclem2  26555  caures  26579  ismtyres  26635  imaiinfv  26862  mzpcompact2lem  26932  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  jm2.27dlem1  27205  fnwe2lem2  27251  fnwe2lem3  27252  aomclem6  27259  deg1mhm  27629  hausgraph  27634  stoweidlem28  27880  afvres  28140  injresinj  28215  redwlk  28364  bnj1379  29179  bnj1253  29363  bnj1280  29366  diaintclN  31870  dibintclN  31979  dihintcl  32156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-xp 4711  df-res 4717  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator