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 3083 . . . . 5  |-  x  e. 
_V
21brres 5130 . . . 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 2488 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872   class class class wbr 4423    |` cres 4855   iotacio 5563   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-xp 4859  df-res 4865  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  7050  smores  7082  smores2  7084  tfrlem1  7105  tz7.44-2  7136  fr0g  7164  frsuc  7165  tz7.48lem  7169  seqomlem1  7178  seqomlem2  7179  seqomlem3  7180  seqomlem4  7181  onasuc  7241  onmsuc  7242  onesuc  7243  resixp  7568  fofinf1o  7861  ixpfi2  7881  ordtypelem4  8045  ordtypelem6  8047  ordtypelem7  8048  unxpwdom2  8112  cantnfres  8190  cantnfp1lem3  8193  dfac12lem1  8580  ackbij2lem2  8677  ackbij2lem3  8678  cfsmolem  8707  alephsing  8713  ttukeylem3  8948  fpwwe2lem6  9067  fpwwe2lem8  9069  fpwwe2lem9  9070  canthp1lem2  9085  inar1  9207  addpiord  9316  mulpiord  9317  addpqnq  9370  mulpqnq  9373  fseq1p1m1  11875  injresinj  12031  seqfeq2  12242  seqres  12246  seqf1olem2  12259  hashgval  12524  hashinf  12526  hashgval2  12563  hashf1lem1  12622  seqcoll  12631  swrdccat1  12815  shftidt  13145  rlimres  13621  lo1res  13622  climres  13638  isercolllem3  13729  fsumss  13790  isumclim3  13819  fsum2dlem  13830  ackbijnn  13885  fprodss  14001  fprod2dlem  14033  iprodclim3  14052  bpolylem  14100  fprodefsum  14148  reeff1  14173  bitsf1  14419  sadcaddlem  14430  sadcadd  14431  sadadd2  14433  sadaddlem  14439  sadasslem  14443  sadeq  14445  eucalgcvga  14544  eucalg  14545  unbenlem  14851  strfv2d  15154  setsid  15163  setsnid  15164  funcres  15800  dmaf  15943  cdaf  15944  1stf1  16076  2ndf1  16079  1stfcl  16081  2ndfcl  16082  prf1st  16088  prf2nd  16089  1st2ndprf  16090  uncf2  16121  diag12  16128  diag2  16129  curf2ndf  16131  yonedalem22  16162  lubval  16229  glbval  16242  resmhm  16605  resghm  16898  efgsres  17387  efgredlemd  17393  efgredlem  17396  gsumzaddlem  17553  dprdfadd  17652  dprdres  17660  dmdprdsplitlem  17669  dprdcntz2  17670  dmdprdsplit2lem  17677  dprdsplit  17680  dpjidcl  17690  ablfac1eu  17705  mgpf  17791  prdscrngd  17840  abvres  18066  reslmhm  18274  ltbwe  18695  subrgascl  18720  subrgasclcl  18721  znf1o  19120  znunithash  19133  psgndiflemB  19166  smadiadetlem3  19691  cnpresti  20302  cnprest  20303  lmres  20314  tx1cn  20622  tx2cn  20623  upxp  20636  uptx  20638  ptrescn  20652  txkgen  20665  cnmpt1st  20681  cnmpt2nd  20682  ptuncnv  20820  ptunhmeo  20821  cnextfres1  21081  prdstmdd  21136  prdsxmslem2  21542  subgnm2  21640  remetdval  21805  rescncf  21927  lmle  22269  lmcau  22280  ovoliunlem1  22453  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  mblvol  22482  mbflimsup  22621  mbflimsupOLD  22622  limcdif  22829  limcres  22839  dvreslem  22862  dvres2lem  22863  dvlip  22943  dvlipcn  22944  dvlip2  22945  c1liplem1  22946  c1lip1  22947  c1lip3  22949  dvgt0lem1  22952  dvivthlem1  22958  lhop1lem  22963  lhop  22966  dvcnvrelem1  22967  dvcvx  22970  ftc2ditglem  22995  itgsubstlem  22998  plyreres  23234  plyexmo  23264  aannenlem1  23282  taylthlem2  23327  ulmres  23341  ulmss  23350  psercn  23379  pserdvlem2  23381  reeff1o  23400  reefiso  23401  efcvx  23402  reefgim  23403  recosf1o  23482  resinf1o  23483  efif1olem4  23492  eff1olem  23495  relogcl  23523  eflog  23524  logef  23529  logeftb  23531  logltb  23547  logcn  23590  advlog  23597  advlogexp  23598  logtayl  23603  logccv  23606  dvcxp1  23678  dvcncxp1  23681  cxpcn  23683  loglesqrt  23696  asinrebnd  23825  dvatan  23859  leibpi  23866  efrlim  23893  jensen  23912  amgmlem  23913  lgamgulmlem2  23953  lgamcvg2  23978  wilthlem3  23993  ftalem3  23997  dvdsmulf1o  24121  fsumdvdsmul  24122  dchrelbas2  24163  dchrabs  24186  sum2dchr  24200  dchrisumlem1  24325  logdivsum  24369  log2sumbnd  24380  ostth2  24473  ostth  24475  redwlk  25334  eupares  25701  ghsubgolemOLD  26096  sspnval  26374  hhssnv  26913  hhssmetdval  26927  foresf1o  28138  ofresid  28245  1stpreimas  28288  xpinpreima  28720  xpinpreima2  28721  cnre2csqlem  28724  rmulccn  28742  zzsnm  28773  cnzh  28782  rezh  28783  measres  29052  cntmeas  29056  cntnevol  29058  1stmbfm  29090  2ndmbfm  29091  carsggect  29158  omsmeas  29163  omsmeasOLD  29164  eulerpartgbij  29213  eulerpartlemgvv  29217  eulerpartlemgs2  29221  iwrdsplit  29228  fibp1  29242  coinfliplem  29319  coinflipprob  29320  gsumnunsn  29433  plyrecld  29446  signstres  29472  bnj1379  29650  bnj1253  29834  bnj1280  29837  subfacp1lem3  29913  subfacp1lem5  29915  erdszelem8  29929  txsconlem  29971  cvmfolem  30010  cvmliftmolem1  30012  cvmliftlem6  30021  cvmliftlem7  30022  cvmliftlem9  30024  mrsubff1  30160  msubff1  30202  fvresval  30415  dfrdg2  30449  frrlem4  30524  sltres  30558  nodense  30583  funpartfv  30717  filnetlem4  31042  icoreunrn  31726  finixpnum  31894  poimirlem3  31907  poimirlem4  31908  poimirlem8  31912  poimirlem26  31930  poimirlem27  31931  itg2gt0cn  31961  areacirclem2  31997  areacirclem4  31999  eqfnun  32012  sdclem2  32035  caures  32053  ismtyres  32104  diaintclN  34595  dibintclN  34704  dihintcl  34881  imaiinfv  35504  mzpcompact2lem  35562  2rexfrabdioph  35608  3rexfrabdioph  35609  4rexfrabdioph  35610  6rexfrabdioph  35611  7rexfrabdioph  35612  jm2.27dlem1  35834  fnwe2lem2  35879  fnwe2lem3  35880  aomclem6  35887  deg1mhm  36054  hausgraph  36059  radcnvrat  36633  wessf1ornlem  37420  mccllem  37617  limcperiod  37648  limcleqr  37665  limclner  37672  resincncf  37692  cncfperiod  37696  icccncfext  37705  cncfiooicclem1  37711  dvbdfbdioolem1  37740  dvnprodlem1  37761  dvnprodlem2  37762  itgioocnicc  37794  stoweidlem28  37828  fourierdlem18  37927  fourierdlem40  37950  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem46  37956  fourierdlem51  37961  fourierdlem70  37980  fourierdlem71  37981  fourierdlem73  37983  fourierdlem74  37984  fourierdlem75  37985  fourierdlem76  37986  fourierdlem78  37988  fourierdlem80  37990  fourierdlem81  37991  fourierdlem82  37992  fourierdlem84  37994  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem92  38002  fourierdlem93  38003  fourierdlem94  38004  fourierdlem101  38011  fourierdlem103  38013  fourierdlem104  38014  fourierdlem111  38021  fourierdlem112  38022  fourierdlem113  38023  sge0tsms  38130  sge0f1o  38132  sge0sup  38141  sge0less  38142  sge0ltfirp  38150  sge0resrnlem  38153  sge0resplit  38156  sge0le  38157  sge0split  38159  sge0fodjrnlem  38166  sge0iun  38169  meadjun  38208  meadjiunlem  38211  psmeasurelem  38216  caratheodory  38257  hoidmvlelem2  38322  hoidmvlelem3  38323  hoidmvlelem4  38324  afvres  38544  iccpartres  38602  iccelpart  38617  pfxccat1  38821  uhgrspansubgrlem  39133  resmgmhm  39417  rhmsubclem2  39708  rhmsubcALTVlem2  39727  lincdifsn  39838  lindslinindimp2lem4  39875  lindslinindsimp2lem5  39876  lincresunit3lem2  39894  fdivmpt  39972
  Copyright terms: Public domain W3C validator