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

Theorem fvres 5895
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 3090 . . . . 5  |-  x  e. 
_V
21brres 5131 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 914 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5586 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5609 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5609 . 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 setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1870   class class class wbr 4426    |` cres 4856   iotacio 5563   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-xp 4860  df-res 4866  df-iota 5565  df-fv 5609
This theorem is referenced by:  funssfv  5896  fveqres  5915  feqresmpt  5935  dffv2  5954  fvreseq0  5997  respreima  6024  fveqressseq  6033  ffvresb  6069  fnressn  6091  fressnfv  6093  fvressn  6095  fvresi  6105  fvsnun1  6114  fvsnun2  6115  fsnunfv  6119  funfvima  6155  funiunfv  6168  soisores  6233  isores3  6241  isoini2  6245  ovres  6450  ofres  6561  f1oweALT  6791  offres  6802  fo1stres  6831  fo2ndres  6832  curry1  6899  curry2  6902  fparlem1  6907  fparlem2  6908  fo2ndf  6914  f1o2ndf1  6915  fnsuppres  6953  wfrlem4  7047  smores  7079  smores2  7081  tfrlem1  7102  tz7.44-2  7133  fr0g  7161  frsuc  7162  tz7.48lem  7166  seqomlem1  7175  seqomlem2  7176  seqomlem3  7177  seqomlem4  7178  onasuc  7238  onmsuc  7239  onesuc  7240  resixp  7565  fofinf1o  7858  ixpfi2  7878  ordtypelem4  8036  ordtypelem6  8038  ordtypelem7  8039  unxpwdom2  8103  cantnfres  8181  cantnfp1lem3  8184  dfac12lem1  8571  ackbij2lem2  8668  ackbij2lem3  8669  cfsmolem  8698  alephsing  8704  ttukeylem3  8939  fpwwe2lem6  9059  fpwwe2lem8  9061  fpwwe2lem9  9062  canthp1lem2  9077  inar1  9199  addpiord  9308  mulpiord  9309  addpqnq  9362  mulpqnq  9365  fseq1p1m1  11866  injresinj  12022  seqfeq2  12233  seqres  12237  seqf1olem2  12250  hashgval  12515  hashinf  12517  hashgval2  12554  hashf1lem1  12613  seqcoll  12621  swrdccat1  12798  shftidt  13124  rlimres  13600  lo1res  13601  climres  13617  isercolllem3  13708  fsumss  13769  isumclim3  13798  fsum2dlem  13809  ackbijnn  13864  fprodss  13980  fprod2dlem  14012  iprodclim3  14031  bpolylem  14079  fprodefsum  14127  reeff1  14152  bitsf1  14394  sadcaddlem  14405  sadcadd  14406  sadadd2  14408  sadaddlem  14414  sadasslem  14418  sadeq  14420  eucalgcvga  14516  eucalg  14517  unbenlem  14806  strfv2d  15109  setsid  15118  setsnid  15119  funcres  15743  dmaf  15886  cdaf  15887  1stf1  16019  2ndf1  16022  1stfcl  16024  2ndfcl  16025  prf1st  16031  prf2nd  16032  1st2ndprf  16033  uncf2  16064  diag12  16071  diag2  16072  curf2ndf  16074  yonedalem22  16105  lubval  16172  glbval  16185  resmhm  16548  resghm  16841  efgsres  17314  efgredlemd  17320  efgredlem  17323  gsumzaddlem  17480  dprdfadd  17579  dprdres  17587  dmdprdsplitlem  17596  dprdcntz2  17597  dmdprdsplit2lem  17604  dprdsplit  17607  dpjidcl  17617  ablfac1eu  17632  mgpf  17718  prdscrngd  17767  abvres  17993  reslmhm  18201  ltbwe  18622  subrgascl  18647  subrgasclcl  18648  znf1o  19044  znunithash  19057  psgndiflemB  19090  smadiadetlem3  19615  cnpresti  20226  cnprest  20227  lmres  20238  tx1cn  20546  tx2cn  20547  upxp  20560  uptx  20562  ptrescn  20576  txkgen  20589  cnmpt1st  20605  cnmpt2nd  20606  ptuncnv  20744  ptunhmeo  20745  cnextfres1  21005  prdstmdd  21060  prdsxmslem2  21466  subgnm2  21564  remetdval  21709  rescncf  21816  lmle  22155  lmcau  22166  ovoliunlem1  22324  ovolicc2lem4  22342  mblvol  22352  mbflimsup  22491  mbflimsupOLD  22492  limcdif  22699  limcres  22709  dvreslem  22732  dvres2lem  22733  dvlip  22813  dvlipcn  22814  dvlip2  22815  c1liplem1  22816  c1lip1  22817  c1lip3  22819  dvgt0lem1  22822  dvivthlem1  22828  lhop1lem  22833  lhop  22836  dvcnvrelem1  22837  dvcvx  22840  ftc2ditglem  22865  itgsubstlem  22868  plyreres  23095  plyexmo  23125  aannenlem1  23140  taylthlem2  23185  ulmres  23199  ulmss  23208  psercn  23237  pserdvlem2  23239  reeff1o  23258  reefiso  23259  efcvx  23260  reefgim  23261  recosf1o  23340  resinf1o  23341  efif1olem4  23350  eff1olem  23353  relogcl  23381  eflog  23382  logef  23387  logeftb  23389  logltb  23405  logcn  23448  advlog  23455  advlogexp  23456  logtayl  23461  logccv  23464  dvcxp1  23536  dvcncxp1  23539  cxpcn  23541  loglesqrt  23554  asinrebnd  23683  dvatan  23717  leibpi  23724  efrlim  23751  jensen  23770  amgmlem  23771  lgamgulmlem2  23811  lgamcvg2  23836  wilthlem3  23851  ftalem3  23855  dvdsmulf1o  23977  fsumdvdsmul  23978  dchrelbas2  24019  dchrabs  24042  sum2dchr  24056  dchrisumlem1  24181  logdivsum  24225  log2sumbnd  24236  ostth2  24329  ostth  24331  redwlk  25172  eupares  25539  ghsubgolemOLD  25934  sspnval  26212  hhssnv  26741  hhssmetdval  26755  foresf1o  27966  ofresid  28074  1stpreimas  28117  xpinpreima  28542  xpinpreima2  28543  cnre2csqlem  28546  rmulccn  28564  zzsnm  28595  cnzh  28604  rezh  28605  measres  28874  cntmeas  28878  cntnevol  28880  1stmbfm  28912  2ndmbfm  28913  carsggect  28970  omsmeas  28975  eulerpartgbij  29022  eulerpartlemgvv  29026  eulerpartlemgs2  29030  iwrdsplit  29037  fibp1  29051  coinfliplem  29128  coinflipprob  29129  gsumnunsn  29204  plyrecld  29217  signstres  29243  bnj1379  29421  bnj1253  29605  bnj1280  29608  subfacp1lem3  29684  subfacp1lem5  29686  erdszelem8  29700  txsconlem  29742  cvmfolem  29781  cvmliftmolem1  29783  cvmliftlem6  29792  cvmliftlem7  29793  cvmliftlem9  29795  mrsubff1  29931  msubff1  29973  fvresval  30186  dfrdg2  30220  frrlem4  30295  sltres  30329  nodense  30354  funpartfv  30488  filnetlem4  30813  icoreunrn  31487  finixpnum  31624  poimirlem3  31637  poimirlem4  31638  poimirlem8  31642  poimirlem26  31660  poimirlem27  31661  itg2gt0cn  31691  areacirclem2  31727  areacirclem4  31729  eqfnun  31742  sdclem2  31765  caures  31783  ismtyres  31834  diaintclN  34325  dibintclN  34434  dihintcl  34611  imaiinfv  35234  mzpcompact2lem  35292  2rexfrabdioph  35338  3rexfrabdioph  35339  4rexfrabdioph  35340  6rexfrabdioph  35341  7rexfrabdioph  35342  jm2.27dlem1  35560  fnwe2lem2  35605  fnwe2lem3  35606  aomclem6  35613  deg1mhm  35773  hausgraph  35778  radcnvrat  36290  wessf1ornlem  37072  mccllem  37239  limcperiod  37270  limcleqr  37287  limclner  37294  resincncf  37314  cncfperiod  37318  icccncfext  37327  cncfiooicclem1  37333  dvbdfbdioolem1  37362  dvnprodlem1  37380  dvnprodlem2  37381  itgioocnicc  37413  stoweidlem28  37447  fourierdlem18  37546  fourierdlem40  37568  fourierdlem42  37570  fourierdlem46  37574  fourierdlem51  37579  fourierdlem70  37598  fourierdlem71  37599  fourierdlem73  37601  fourierdlem74  37602  fourierdlem75  37603  fourierdlem76  37604  fourierdlem78  37606  fourierdlem80  37608  fourierdlem81  37609  fourierdlem82  37610  fourierdlem84  37612  fourierdlem89  37617  fourierdlem90  37618  fourierdlem91  37619  fourierdlem92  37620  fourierdlem93  37621  fourierdlem94  37622  fourierdlem101  37629  fourierdlem103  37631  fourierdlem104  37632  fourierdlem111  37639  fourierdlem112  37640  fourierdlem113  37641  sge0tsms  37746  sge0f1o  37748  sge0sup  37757  sge0less  37758  sge0ltfirp  37766  sge0resrnlem  37769  sge0resplit  37772  sge0le  37773  sge0split  37775  sge0fodjrnlem  37782  sge0iun  37785  meadjun  37799  meadjiunlem  37802  psmeasurelem  37807  caratheodory  37848  afvres  38054  iccpartres  38112  iccelpart  38127  pfxccat1  38331  resmgmhm  38546  rhmsubclem2  38837  rhmsubcALTVlem2  38856  lincdifsn  38967  lindslinindimp2lem4  39004  lindslinindsimp2lem5  39005  lincresunit3lem2  39023  fdivmpt  39102
  Copyright terms: Public domain W3C validator