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

Theorem fvres 5878
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 3116 . . . . 5  |-  x  e. 
_V
21brres 5278 . . . 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 5570 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5594 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5594 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2533 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   class class class wbr 4447    |` cres 5001   iotacio 5547   ` cfv 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-xp 5005  df-res 5011  df-iota 5549  df-fv 5594
This theorem is referenced by:  funssfv  5879  fveqres  5898  feqresmpt  5919  dffv2  5938  fvreseq0  5979  respreima  6008  ffvresb  6050  fnressn  6071  fressnfv  6073  fvressn  6075  fvresi  6085  fvunsn  6091  fvsnun1  6094  fvsnun2  6095  fsnunfv  6099  fnsuppresOLD  6119  funfvima  6133  funiunfv  6146  soisores  6209  isores3  6217  isoini2  6221  ovres  6424  ofres  6537  f1oweALT  6765  offres  6776  fo1stres  6805  fo2ndres  6806  curry1  6872  curry2  6875  fparlem1  6880  fparlem2  6881  fo2ndf  6887  f1o2ndf1  6888  fnsuppres  6924  smores  7020  smores2  7022  tfrlem1  7042  tz7.44-2  7070  fr0g  7098  frsuc  7099  tz7.48lem  7103  seqomlem1  7112  seqomlem2  7113  seqomlem3  7114  seqomlem4  7115  onasuc  7175  onmsuc  7176  onesuc  7177  resixp  7501  fofinf1o  7797  ixpfi2  7814  ordtypelem4  7942  ordtypelem6  7944  ordtypelem7  7945  unxpwdom2  8010  cantnfres  8092  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  dfac12lem1  8519  ackbij2lem2  8616  ackbij2lem3  8617  cfsmolem  8646  alephsing  8652  ttukeylem3  8887  fpwwe2lem6  9009  fpwwe2lem8  9011  fpwwe2lem9  9012  canthp1lem2  9027  inar1  9149  addpiord  9258  mulpiord  9259  addpqnq  9312  mulpqnq  9315  fseq1p1m1  11748  injresinj  11890  seqfeq2  12093  seqres  12097  seqf1olem2  12110  hashgval  12370  hashinf  12372  hashgval2  12408  hashf1lem1  12464  seqcoll  12472  swrdccat1  12639  shftidt  12872  rlimres  13337  lo1res  13338  climres  13354  isercolllem3  13445  fsumss  13503  isumclim3  13530  fsum2dlem  13541  ackbijnn  13596  reeff1  13709  bitsf1  13948  sadcaddlem  13959  sadcadd  13960  sadadd2  13962  sadaddlem  13968  sadasslem  13972  sadeq  13974  eucalgcvga  14067  eucalg  14068  unbenlem  14278  strfv2d  14515  setsid  14524  setsnid  14525  funcres  15116  dmaf  15227  cdaf  15228  1stf1  15312  2ndf1  15315  1stfcl  15317  2ndfcl  15318  prf1st  15324  prf2nd  15325  1st2ndprf  15326  uncf2  15357  diag12  15364  diag2  15365  curf2ndf  15367  yonedalem22  15398  lubval  15464  glbval  15477  resmhm  15797  resghm  16075  efgsres  16549  efgredlemd  16555  efgredlem  16558  gsumzaddlem  16722  gsumzaddlemOLD  16724  dprdfadd  16847  dprdfaddOLD  16854  dprdres  16862  dmdprdsplitlem  16871  dmdprdsplitlemOLD  16872  dprdcntz2  16873  dmdprdsplit2lem  16881  dprdsplit  16884  dpjidcl  16894  dpjidclOLD  16901  ablfac1eu  16911  mgpf  16994  prdscrngd  17043  abvres  17268  reslmhm  17478  ltbwe  17905  subrgascl  17931  subrgasclcl  17932  znf1o  18354  znunithash  18367  psgndiflemB  18400  smadiadetlem3  18934  cnpresti  19552  cnprest  19553  lmres  19564  tx1cn  19842  tx2cn  19843  upxp  19856  uptx  19858  ptrescn  19872  txkgen  19885  cnmpt1st  19901  cnmpt2nd  19902  ptuncnv  20040  ptunhmeo  20041  cnextfres  20300  prdstmdd  20354  prdsxmslem2  20764  subgnm2  20880  remetdval  21026  rescncf  21133  lmle  21472  lmcau  21483  ovoliunlem1  21645  ovolicc2lem4  21663  mblvol  21673  mbflimsup  21805  limcdif  22012  limcres  22022  dvreslem  22045  dvres2lem  22046  dvlip  22126  dvlipcn  22127  dvlip2  22128  c1liplem1  22129  c1lip1  22130  c1lip3  22132  dvgt0lem1  22135  dvivthlem1  22141  lhop1lem  22146  lhop  22149  dvcnvrelem1  22150  dvcvx  22153  ftc2ditglem  22178  itgsubstlem  22181  plyreres  22410  plyexmo  22440  aannenlem1  22455  taylthlem2  22500  ulmres  22514  ulmss  22523  psercn  22552  pserdvlem2  22554  reeff1o  22573  reefiso  22574  efcvx  22575  reefgim  22576  recosf1o  22652  resinf1o  22653  efif1olem4  22662  eff1olem  22665  relogcl  22688  eflog  22689  logef  22691  logeftb  22693  logltb  22709  logcn  22753  advlog  22760  advlogexp  22761  logtayl  22766  logccv  22769  dvcxp1  22841  cxpcn  22844  loglesqrt  22857  asinrebnd  22957  dvatan  22991  leibpi  22998  efrlim  23024  jensen  23043  amgmlem  23044  wilthlem3  23069  ftalem3  23073  dvdsmulf1o  23195  fsumdvdsmul  23196  dchrelbas2  23237  dchrabs  23260  sum2dchr  23274  dchrisumlem1  23399  logdivsum  23443  log2sumbnd  23454  ostth2  23547  ostth  23549  redwlk  24281  eupares  24648  ghsubgolem  25045  sspnval  25323  hhssnv  25853  hhssmetdval  25867  ofresid  27152  xpinpreima  27521  xpinpreima2  27522  cnre2csqlem  27525  rmulccn  27543  zzsnm  27574  zzsnmOLD  27575  cnzh  27584  rezh  27585  measres  27830  cntmeas  27834  cntnevol  27836  1stmbfm  27868  2ndmbfm  27869  eulerpartgbij  27948  eulerpartlemgvv  27952  eulerpartlemgs2  27956  iwrdsplit  27963  fibp1  27977  coinfliplem  28054  coinflipprob  28055  gsumnunsn  28130  plyrecld  28143  signstres  28169  lgamgulmlem2  28209  lgamcvg2  28234  subfacp1lem3  28263  subfacp1lem5  28265  erdszelem8  28279  txsconlem  28322  cvmfolem  28361  cvmliftmolem1  28363  cvmliftlem6  28372  cvmliftlem7  28373  cvmliftlem9  28375  fprodss  28654  fprodefsum  28678  fprod2dlem  28684  iprodclim3  28693  fvresval  28771  dfrdg2  28802  wfrlem4  28920  frrlem4  28964  sltres  28998  nodense  29023  funpartfv  29169  bpolylem  29384  finixpnum  29612  itg2gt0cn  29645  dvcncxp1  29675  areacirclem2  29683  areacirclem4  29685  filnetlem4  29800  eqfnun  29813  sdclem2  29836  caures  29854  ismtyres  29905  imaiinfv  30227  mzpcompact2lem  30286  2rexfrabdioph  30331  3rexfrabdioph  30332  4rexfrabdioph  30333  6rexfrabdioph  30334  7rexfrabdioph  30335  jm2.27dlem1  30555  fnwe2lem2  30601  fnwe2lem3  30602  aomclem6  30609  deg1mhm  30772  hausgraph  30777  limcperiod  31170  limcleqr  31186  limclner  31193  resincncf  31213  cncfperiod  31217  icccncfext  31226  cncfiooicclem1  31232  dvbdfbdioolem1  31258  itgioocnicc  31295  stoweidlem28  31328  fourierdlem18  31425  fourierdlem40  31447  fourierdlem42  31449  fourierdlem46  31453  fourierdlem51  31458  fourierdlem70  31477  fourierdlem71  31478  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem80  31487  fourierdlem81  31488  fourierdlem82  31489  fourierdlem84  31491  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem92  31499  fourierdlem93  31500  fourierdlem94  31501  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  afvres  31724  lincdifsn  32098  lindslinindimp2lem4  32135  lindslinindsimp2lem5  32136  lincresunit3lem2  32154  bnj1379  32968  bnj1253  33152  bnj1280  33155  diaintclN  35855  dibintclN  35964  dihintcl  36141
  Copyright terms: Public domain W3C validator