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

Theorem fvres 5747
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 2961 . . . . 5  |-  x  e. 
_V
21brres 5154 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 875 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5441 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5464 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5464 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2495 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   class class class wbr 4214    |` cres 4882   iotacio 5418   ` cfv 5456
This theorem is referenced by:  funssfv  5748  fveqres  5766  feqresmpt  5782  dffv2  5798  fvreseq  5835  respreima  5861  ffvresb  5902  fnressn  5920  fressnfv  5922  fvresi  5926  fvunsn  5927  fvsnun1  5930  fvsnun2  5931  fsnunfv  5935  fnsuppres  5954  funfvima  5975  funiunfv  5997  soisores  6049  isores3  6057  isoini2  6061  f1oweALT  6076  ovres  6215  offres  6321  ofres  6323  fo1stres  6372  fo2ndres  6373  curry1  6440  curry2  6443  fparlem1  6448  fparlem2  6449  fo2ndf  6455  f1o2ndf1  6456  smores  6616  smores2  6618  tfrlem5  6643  tz7.44-2  6667  fr0g  6695  frsuc  6696  tz7.48lem  6700  seqomlem1  6709  seqomlem2  6710  seqomlem3  6711  seqomlem4  6712  onasuc  6774  onmsuc  6775  onesuc  6776  resixp  7099  fofinf1o  7389  ixpfi2  7407  ordtypelem4  7492  ordtypelem6  7494  ordtypelem7  7495  unxpwdom2  7558  cantnfres  7635  cantnfp1lem3  7638  dfac12lem1  8025  ackbij2lem2  8122  ackbij2lem3  8123  cfsmolem  8152  alephsing  8158  ttukeylem3  8393  fpwwe2lem6  8512  fpwwe2lem8  8514  fpwwe2lem9  8515  canthp1lem2  8530  inar1  8652  addpiord  8763  mulpiord  8764  addpqnq  8817  mulpqnq  8820  fseq1p1m1  11124  injresinj  11202  seqfeq2  11348  seqres  11352  seqf1olem2  11365  hashgval  11623  hashinf  11625  hashgval2  11654  hashf1lem1  11706  seqcoll  11714  swrdccat1  11776  shftidt  11899  rlimres  12354  lo1res  12355  climres  12371  isercolllem3  12462  fsumss  12521  isumclim3  12545  fsum2dlem  12556  ackbijnn  12609  reeff1  12723  bitsf1  12960  sadcaddlem  12971  sadcadd  12972  sadadd2  12974  sadaddlem  12980  sadasslem  12984  sadeq  12986  eucalgcvga  13079  eucalg  13080  unbenlem  13278  strfv2d  13501  setsid  13510  setsnid  13511  funcres  14095  dmaf  14206  cdaf  14207  1stf1  14291  2ndf1  14294  1stfcl  14296  2ndfcl  14297  prf1st  14303  prf2nd  14304  1st2ndprf  14305  uncf2  14336  diag12  14343  diag2  14344  curf2ndf  14346  yonedalem22  14377  resmhm  14761  resghm  15024  efgsres  15372  efgredlemd  15378  efgredlem  15381  gsumzaddlem  15528  dprdfadd  15580  dprdres  15588  dmdprdsplitlem  15597  dprdcntz2  15598  dmdprdsplit2lem  15605  dprdsplit  15608  dpjidcl  15618  ablfac1eu  15633  mgpf  15677  prdscrngd  15721  abvres  15929  reslmhm  16130  ltbwe  16535  subrgascl  16560  subrgasclcl  16561  znf1o  16834  znunithash  16847  cnpresti  17354  cnprest  17355  lmres  17366  tx1cn  17643  tx2cn  17644  upxp  17657  uptx  17659  ptrescn  17673  txkgen  17686  cnmpt1st  17702  cnmpt2nd  17703  ptuncnv  17841  ptunhmeo  17842  cnextfres  18101  prdstmdd  18155  prdsxmslem2  18561  subgnm2  18677  remetdval  18822  rescncf  18929  lmle  19256  lmcau  19267  ovoliunlem1  19400  ovolicc2lem4  19418  mblvol  19428  mbflimsup  19560  limcdif  19765  limcres  19775  dvreslem  19798  dvres2lem  19799  dvlip  19879  dvlipcn  19880  dvlip2  19881  c1liplem1  19882  c1lip1  19883  c1lip3  19885  dvgt0lem1  19888  dvivthlem1  19894  lhop1lem  19899  lhop  19902  dvcnvrelem1  19903  dvcvx  19906  ftc2ditglem  19931  itgsubstlem  19934  plyreres  20202  plyexmo  20232  aannenlem1  20247  taylthlem2  20292  ulmres  20306  ulmss  20315  psercn  20344  pserdvlem2  20346  reeff1o  20365  reefiso  20366  efcvx  20367  reefgim  20368  recosf1o  20439  resinf1o  20440  efif1olem4  20449  eff1olem  20452  relogcl  20475  eflog  20476  logef  20478  logeftb  20480  logltb  20496  logcn  20540  advlog  20547  advlogexp  20548  logtayl  20553  logccv  20556  dvcxp1  20628  cxpcn  20631  loglesqr  20644  asinrebnd  20743  dvatan  20777  leibpi  20784  efrlim  20810  jensen  20829  amgmlem  20830  wilthlem3  20855  ftalem3  20859  dvdsmulf1o  20981  fsumdvdsmul  20982  dchrelbas2  21023  dchrabs  21046  sum2dchr  21060  dchrisumlem1  21185  logdivsum  21229  log2sumbnd  21240  ostth2  21333  ostth  21335  redwlk  21608  eupares  21699  ghsubgolem  21960  sspnval  22238  hhssnv  22766  hhssmetdval  22780  ofresid  24057  xpinpreima  24306  xpinpreima2  24307  cnre2csqlem  24310  rmulccn  24316  zzsnm  24344  cnzh  24356  rezh  24357  measres  24578  cntmeas  24582  cntnevol  24584  1stmbfm  24612  2ndmbfm  24613  coinfliplem  24738  coinflipprob  24739  lgamgulmlem2  24816  lgamcvg2  24841  subfacp1lem3  24870  subfacp1lem5  24872  erdszelem8  24886  txsconlem  24929  cvmfolem  24968  cvmliftmolem1  24970  cvmliftlem6  24979  cvmliftlem7  24980  cvmliftlem9  24982  fprodss  25276  fprodefsum  25300  fprod2dlem  25306  iprodclim3  25315  fvresval  25393  dfrdg2  25425  wfrlem4  25543  frrlem4  25587  sltres  25621  nodense  25646  funpartfv  25792  bpolylem  26096  itg2gt0cn  26262  areacirclem2  26295  areacirclem4  26297  filnetlem4  26412  eqfnun  26425  sdclem2  26448  caures  26468  ismtyres  26519  imaiinfv  26742  mzpcompact2lem  26810  2rexfrabdioph  26858  3rexfrabdioph  26859  4rexfrabdioph  26860  6rexfrabdioph  26861  7rexfrabdioph  26862  jm2.27dlem1  27082  fnwe2lem2  27128  fnwe2lem3  27129  aomclem6  27136  deg1mhm  27505  hausgraph  27510  stoweidlem28  27755  afvres  28014  swrd0swrd  28219  bnj1379  29264  bnj1253  29448  bnj1280  29451  diaintclN  31918  dibintclN  32027  dihintcl  32204
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-xp 4886  df-res 4892  df-iota 5420  df-fv 5464
  Copyright terms: Public domain W3C validator