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

Theorem fvres 5906
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 3060 . . . . 5  |-  x  e. 
_V
21brres 5133 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 922 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5590 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5613 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5613 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2521 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    e. wcel 1898   class class class wbr 4418    |` cres 4858   iotacio 5567   ` cfv 5605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-xp 4862  df-res 4868  df-iota 5569  df-fv 5613
This theorem is referenced by:  funssfv  5907  fveqres  5926  feqresmpt  5946  dffv2  5966  fvreseq0  6010  respreima  6037  fveqressseq  6046  ffvresb  6083  fnressn  6105  fressnfv  6107  fvressn  6109  fvresi  6119  fvsnun1  6128  fvsnun2  6129  fsnunfv  6133  funfvima  6170  funiunfv  6183  soisores  6248  isores3  6256  isoini2  6260  ovres  6468  ofres  6579  f1oweALT  6809  offres  6820  fo1stres  6849  fo2ndres  6850  curry1  6920  curry2  6923  fparlem1  6928  fparlem2  6929  fo2ndf  6935  f1o2ndf1  6936  fnsuppres  6974  wfrlem4  7070  smores  7102  smores2  7104  tfrlem1  7125  tz7.44-2  7156  fr0g  7184  frsuc  7185  tz7.48lem  7189  seqomlem1  7198  seqomlem2  7199  seqomlem3  7200  seqomlem4  7201  onasuc  7261  onmsuc  7262  onesuc  7263  resixp  7588  fofinf1o  7883  ixpfi2  7903  ordtypelem4  8067  ordtypelem6  8069  ordtypelem7  8070  unxpwdom2  8134  cantnfres  8213  cantnfp1lem3  8216  dfac12lem1  8604  ackbij2lem2  8701  ackbij2lem3  8702  cfsmolem  8731  alephsing  8737  ttukeylem3  8972  fpwwe2lem6  9091  fpwwe2lem8  9093  fpwwe2lem9  9094  canthp1lem2  9109  inar1  9231  addpiord  9340  mulpiord  9341  addpqnq  9394  mulpqnq  9397  fseq1p1m1  11903  injresinj  12063  seqfeq2  12274  seqres  12278  seqf1olem2  12291  hashgval  12556  hashinf  12558  hashgval2  12595  hashf1lem1  12657  seqcoll  12666  swrdccat1  12856  shftidt  13200  rlimres  13677  lo1res  13678  climres  13694  isercolllem3  13785  fsumss  13846  isumclim3  13875  fsum2dlem  13886  ackbijnn  13941  fprodss  14057  fprod2dlem  14089  iprodclim3  14108  bpolylem  14156  fprodefsum  14204  reeff1  14229  bitsf1  14475  sadcaddlem  14486  sadcadd  14487  sadadd2  14489  sadaddlem  14495  sadasslem  14499  sadeq  14501  eucalgcvga  14600  eucalg  14601  unbenlem  14907  strfv2d  15210  setsid  15219  setsnid  15220  funcres  15856  dmaf  15999  cdaf  16000  1stf1  16132  2ndf1  16135  1stfcl  16137  2ndfcl  16138  prf1st  16144  prf2nd  16145  1st2ndprf  16146  uncf2  16177  diag12  16184  diag2  16185  curf2ndf  16187  yonedalem22  16218  lubval  16285  glbval  16298  resmhm  16661  resghm  16954  efgsres  17443  efgredlemd  17449  efgredlem  17452  gsumzaddlem  17609  dprdfadd  17708  dprdres  17716  dmdprdsplitlem  17725  dprdcntz2  17726  dmdprdsplit2lem  17733  dprdsplit  17736  dpjidcl  17746  ablfac1eu  17761  mgpf  17847  prdscrngd  17896  abvres  18122  reslmhm  18330  ltbwe  18751  subrgascl  18776  subrgasclcl  18777  znf1o  19177  znunithash  19190  psgndiflemB  19223  smadiadetlem3  19748  cnpresti  20359  cnprest  20360  lmres  20371  tx1cn  20679  tx2cn  20680  upxp  20693  uptx  20695  ptrescn  20709  txkgen  20722  cnmpt1st  20738  cnmpt2nd  20739  ptuncnv  20877  ptunhmeo  20878  cnextfres1  21138  prdstmdd  21193  prdsxmslem2  21599  subgnm2  21697  remetdval  21862  rescncf  21984  lmle  22326  lmcau  22337  ovoliunlem1  22510  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  mblvol  22539  mbflimsup  22679  mbflimsupOLD  22680  limcdif  22887  limcres  22897  dvreslem  22920  dvres2lem  22921  dvlip  23001  dvlipcn  23002  dvlip2  23003  c1liplem1  23004  c1lip1  23005  c1lip3  23007  dvgt0lem1  23010  dvivthlem1  23016  lhop1lem  23021  lhop  23024  dvcnvrelem1  23025  dvcvx  23028  ftc2ditglem  23053  itgsubstlem  23056  plyreres  23292  plyexmo  23322  aannenlem1  23340  taylthlem2  23385  ulmres  23399  ulmss  23408  psercn  23437  pserdvlem2  23439  reeff1o  23458  reefiso  23459  efcvx  23460  reefgim  23461  recosf1o  23540  resinf1o  23541  efif1olem4  23550  eff1olem  23553  relogcl  23581  eflog  23582  logef  23587  logeftb  23589  logltb  23605  logcn  23648  advlog  23655  advlogexp  23656  logtayl  23661  logccv  23664  dvcxp1  23736  dvcncxp1  23739  cxpcn  23741  loglesqrt  23754  asinrebnd  23883  dvatan  23917  leibpi  23924  efrlim  23951  jensen  23970  amgmlem  23971  lgamgulmlem2  24011  lgamcvg2  24036  wilthlem3  24051  ftalem3  24055  dvdsmulf1o  24179  fsumdvdsmul  24180  dchrelbas2  24221  dchrabs  24244  sum2dchr  24258  dchrisumlem1  24383  logdivsum  24427  log2sumbnd  24438  ostth2  24531  ostth  24533  redwlk  25392  eupares  25759  ghsubgolemOLD  26154  sspnval  26432  hhssnv  26971  hhssmetdval  26985  foresf1o  28195  ofresid  28296  1stpreimas  28338  xpinpreima  28763  xpinpreima2  28764  cnre2csqlem  28767  rmulccn  28785  zzsnm  28816  cnzh  28825  rezh  28826  measres  29095  cntmeas  29099  cntnevol  29101  1stmbfm  29132  2ndmbfm  29133  carsggect  29200  omsmeas  29205  omsmeasOLD  29206  eulerpartgbij  29255  eulerpartlemgvv  29259  eulerpartlemgs2  29263  iwrdsplit  29270  fibp1  29284  coinfliplem  29361  coinflipprob  29362  gsumnunsn  29475  plyrecld  29488  signstres  29514  bnj1379  29692  bnj1253  29876  bnj1280  29879  subfacp1lem3  29955  subfacp1lem5  29957  erdszelem8  29971  txsconlem  30013  cvmfolem  30052  cvmliftmolem1  30054  cvmliftlem6  30063  cvmliftlem7  30064  cvmliftlem9  30066  mrsubff1  30202  msubff1  30244  fvresval  30458  dfrdg2  30492  frrlem4  30567  sltres  30601  nodense  30628  funpartfv  30762  filnetlem4  31087  icoreunrn  31808  finixpnum  31976  poimirlem3  31989  poimirlem4  31990  poimirlem8  31994  poimirlem26  32012  poimirlem27  32013  itg2gt0cn  32043  areacirclem2  32079  areacirclem4  32081  eqfnun  32094  sdclem2  32117  caures  32135  ismtyres  32186  diaintclN  34672  dibintclN  34781  dihintcl  34958  imaiinfv  35581  mzpcompact2lem  35639  2rexfrabdioph  35685  3rexfrabdioph  35686  4rexfrabdioph  35687  6rexfrabdioph  35688  7rexfrabdioph  35689  jm2.27dlem1  35910  fnwe2lem2  35955  fnwe2lem3  35956  aomclem6  35963  deg1mhm  36130  hausgraph  36135  radcnvrat  36708  wessf1ornlem  37513  mccllem  37763  limcperiod  37794  limcleqr  37811  limclner  37818  resincncf  37838  cncfperiod  37842  icccncfext  37851  cncfiooicclem1  37857  dvbdfbdioolem1  37886  dvnprodlem1  37907  dvnprodlem2  37908  itgioocnicc  37940  stoweidlem28  37989  fourierdlem18  38088  fourierdlem40  38111  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem46  38117  fourierdlem51  38122  fourierdlem70  38141  fourierdlem71  38142  fourierdlem73  38144  fourierdlem74  38145  fourierdlem75  38146  fourierdlem76  38147  fourierdlem78  38149  fourierdlem80  38151  fourierdlem81  38152  fourierdlem82  38153  fourierdlem84  38155  fourierdlem89  38160  fourierdlem90  38161  fourierdlem91  38162  fourierdlem92  38163  fourierdlem93  38164  fourierdlem94  38165  fourierdlem101  38172  fourierdlem103  38174  fourierdlem104  38175  fourierdlem111  38182  fourierdlem112  38183  fourierdlem113  38184  sge0tsms  38325  sge0f1o  38327  sge0sup  38336  sge0less  38337  sge0ltfirp  38345  sge0resrnlem  38348  sge0resplit  38351  sge0le  38352  sge0split  38354  sge0fodjrnlem  38361  sge0iun  38364  meadjun  38405  meadjiunlem  38408  psmeasurelem  38413  caratheodory  38457  hoidmvlelem2  38525  hoidmvlelem3  38526  hoidmvlelem4  38527  voncmpl  38550  mblvon  38568  afvres  38809  iccpartres  38867  iccelpart  38882  pfxccat1  39088  uhgrspansubgrlem  39508  red1wlk  39813  pthdivtx  39858  pthdlem1  39888  resmgmhm  40167  rhmsubclem2  40458  rhmsubcALTVlem2  40477  lincdifsn  40586  lindslinindimp2lem4  40623  lindslinindsimp2lem5  40624  lincresunit3lem2  40642  fdivmpt  40720
  Copyright terms: Public domain W3C validator