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

Theorem fvres 5692
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 2965 . . . . 5  |-  x  e. 
_V
21brres 5104 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 891 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5390 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5414 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5414 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2490 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755   class class class wbr 4280    |` cres 4829   iotacio 5367   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-xp 4833  df-res 4839  df-iota 5369  df-fv 5414
This theorem is referenced by:  funssfv  5693  fveqres  5712  feqresmpt  5733  dffv2  5752  fvreseq0  5791  respreima  5820  ffvresb  5861  fnressn  5881  fressnfv  5883  fvresi  5891  fvunsn  5897  fvsnun1  5900  fvsnun2  5901  fsnunfv  5905  fnsuppresOLD  5925  funfvima  5939  funiunfv  5952  soisores  6005  isores3  6013  isoini2  6017  ovres  6219  ofres  6324  f1oweALT  6550  offres  6561  fo1stres  6589  fo2ndres  6590  curry1  6653  curry2  6656  fparlem1  6661  fparlem2  6662  fo2ndf  6668  f1o2ndf1  6669  fnsuppres  6705  smores  6799  smores2  6801  tfrlem1  6821  tz7.44-2  6849  fr0g  6877  frsuc  6878  tz7.48lem  6882  seqomlem1  6891  seqomlem2  6892  seqomlem3  6893  seqomlem4  6894  onasuc  6956  onmsuc  6957  onesuc  6958  resixp  7286  fofinf1o  7580  ixpfi2  7597  ordtypelem4  7723  ordtypelem6  7725  ordtypelem7  7726  unxpwdom2  7791  cantnfres  7873  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  dfac12lem1  8300  ackbij2lem2  8397  ackbij2lem3  8398  cfsmolem  8427  alephsing  8433  ttukeylem3  8668  fpwwe2lem6  8790  fpwwe2lem8  8792  fpwwe2lem9  8793  canthp1lem2  8808  inar1  8930  addpiord  9041  mulpiord  9042  addpqnq  9095  mulpqnq  9098  fseq1p1m1  11518  injresinj  11623  seqfeq2  11813  seqres  11817  seqf1olem2  11830  hashgval  12090  hashinf  12092  hashgval2  12125  hashf1lem1  12192  seqcoll  12200  swrdccat1  12335  shftidt  12555  rlimres  13020  lo1res  13021  climres  13037  isercolllem3  13128  fsumss  13186  isumclim3  13210  fsum2dlem  13221  ackbijnn  13274  reeff1  13387  bitsf1  13625  sadcaddlem  13636  sadcadd  13637  sadadd2  13639  sadaddlem  13645  sadasslem  13649  sadeq  13651  eucalgcvga  13744  eucalg  13745  unbenlem  13952  strfv2d  14189  setsid  14198  setsnid  14199  funcres  14789  dmaf  14900  cdaf  14901  1stf1  14985  2ndf1  14988  1stfcl  14990  2ndfcl  14991  prf1st  14997  prf2nd  14998  1st2ndprf  14999  uncf2  15030  diag12  15037  diag2  15038  curf2ndf  15040  yonedalem22  15071  lubval  15137  glbval  15150  resmhm  15469  resghm  15743  efgsres  16215  efgredlemd  16221  efgredlem  16224  gsumzaddlem  16388  gsumzaddlemOLD  16390  dprdfadd  16484  dprdfaddOLD  16491  dprdres  16499  dmdprdsplitlem  16508  dmdprdsplitlemOLD  16509  dprdcntz2  16510  dmdprdsplit2lem  16518  dprdsplit  16521  dpjidcl  16531  dpjidclOLD  16538  ablfac1eu  16548  mgpf  16592  prdscrngd  16640  abvres  16848  reslmhm  17055  ltbwe  17486  subrgascl  17512  subrgasclcl  17513  znf1o  17826  znunithash  17839  psgndiflemB  17872  smadiadetlem3  18316  cnpresti  18734  cnprest  18735  lmres  18746  tx1cn  19024  tx2cn  19025  upxp  19038  uptx  19040  ptrescn  19054  txkgen  19067  cnmpt1st  19083  cnmpt2nd  19084  ptuncnv  19222  ptunhmeo  19223  cnextfres  19482  prdstmdd  19536  prdsxmslem2  19946  subgnm2  20062  remetdval  20208  rescncf  20315  lmle  20654  lmcau  20665  ovoliunlem1  20827  ovolicc2lem4  20845  mblvol  20855  mbflimsup  20986  limcdif  21193  limcres  21203  dvreslem  21226  dvres2lem  21227  dvlip  21307  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  c1lip1  21311  c1lip3  21313  dvgt0lem1  21316  dvivthlem1  21322  lhop1lem  21327  lhop  21330  dvcnvrelem1  21331  dvcvx  21334  ftc2ditglem  21359  itgsubstlem  21362  plyreres  21634  plyexmo  21664  aannenlem1  21679  taylthlem2  21724  ulmres  21738  ulmss  21747  psercn  21776  pserdvlem2  21778  reeff1o  21797  reefiso  21798  efcvx  21799  reefgim  21800  recosf1o  21876  resinf1o  21877  efif1olem4  21886  eff1olem  21889  relogcl  21912  eflog  21913  logef  21915  logeftb  21917  logltb  21933  logcn  21977  advlog  21984  advlogexp  21985  logtayl  21990  logccv  21993  dvcxp1  22065  cxpcn  22068  loglesqr  22081  asinrebnd  22181  dvatan  22215  leibpi  22222  efrlim  22248  jensen  22267  amgmlem  22268  wilthlem3  22293  ftalem3  22297  dvdsmulf1o  22419  fsumdvdsmul  22420  dchrelbas2  22461  dchrabs  22484  sum2dchr  22498  dchrisumlem1  22623  logdivsum  22667  log2sumbnd  22678  ostth2  22771  ostth  22773  redwlk  23328  eupares  23419  ghsubgolem  23680  sspnval  23958  hhssnv  24488  hhssmetdval  24502  ofresid  25784  xpinpreima  26190  xpinpreima2  26191  cnre2csqlem  26194  rmulccn  26212  zzsnm  26243  zzsnmOLD  26244  cnzh  26253  rezh  26254  measres  26490  cntmeas  26494  cntnevol  26496  1stmbfm  26529  2ndmbfm  26530  eulerpartgbij  26603  eulerpartlemgvv  26607  eulerpartlemgs2  26611  iwrdsplit  26618  fibp1  26632  coinfliplem  26709  coinflipprob  26710  gsumnunsn  26785  plyrecld  26798  signstres  26824  lgamgulmlem2  26864  lgamcvg2  26889  subfacp1lem3  26918  subfacp1lem5  26920  erdszelem8  26934  txsconlem  26977  cvmfolem  27016  cvmliftmolem1  27018  cvmliftlem6  27027  cvmliftlem7  27028  cvmliftlem9  27030  fprodss  27308  fprodefsum  27332  fprod2dlem  27338  iprodclim3  27347  fvresval  27425  dfrdg2  27456  wfrlem4  27574  frrlem4  27618  sltres  27652  nodense  27677  funpartfv  27823  bpolylem  28038  finixpnum  28258  itg2gt0cn  28291  dvcncxp1  28321  areacirclem2  28329  areacirclem4  28331  filnetlem4  28446  eqfnun  28459  sdclem2  28482  caures  28500  ismtyres  28551  imaiinfv  28874  mzpcompact2lem  28933  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  jm2.27dlem1  29203  fnwe2lem2  29249  fnwe2lem3  29250  aomclem6  29257  deg1mhm  29420  hausgraph  29425  stoweidlem28  29669  afvres  29924  fvressn  29998  lincdifsn  30667  lindslinindimp2lem4  30704  lindslinindsimp2lem5  30705  lincresunit3lem2  30723  bnj1379  31526  bnj1253  31710  bnj1280  31713  diaintclN  34276  dibintclN  34385  dihintcl  34562
  Copyright terms: Public domain W3C validator