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

Theorem fvres 5704
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 2919 . . . . 5  |-  x  e. 
_V
21brres 5111 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 874 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5398 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5421 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5421 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2461 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   class class class wbr 4172    |` cres 4839   iotacio 5375   ` cfv 5413
This theorem is referenced by:  funssfv  5705  fveqres  5723  feqresmpt  5739  dffv2  5755  fvreseq  5792  respreima  5818  ffvresb  5859  fnressn  5877  fressnfv  5879  fvresi  5883  fvunsn  5884  fvsnun1  5887  fvsnun2  5888  fsnunfv  5892  fnsuppres  5911  funfvima  5932  funiunfv  5954  soisores  6006  isores3  6014  isoini2  6018  f1oweALT  6033  ovres  6172  offres  6278  ofres  6280  fo1stres  6329  fo2ndres  6330  curry1  6397  curry2  6400  fparlem1  6405  fparlem2  6406  fo2ndf  6412  f1o2ndf1  6413  smores  6573  smores2  6575  tfrlem5  6600  tz7.44-2  6624  fr0g  6652  frsuc  6653  tz7.48lem  6657  seqomlem1  6666  seqomlem2  6667  seqomlem3  6668  seqomlem4  6669  onasuc  6731  onmsuc  6732  onesuc  6733  resixp  7056  fofinf1o  7346  ixpfi2  7363  ordtypelem4  7446  ordtypelem6  7448  ordtypelem7  7449  unxpwdom2  7512  cantnfres  7589  cantnfp1lem3  7592  dfac12lem1  7979  ackbij2lem2  8076  ackbij2lem3  8077  cfsmolem  8106  alephsing  8112  ttukeylem3  8347  fpwwe2lem6  8466  fpwwe2lem8  8468  fpwwe2lem9  8469  canthp1lem2  8484  inar1  8606  addpiord  8717  mulpiord  8718  addpqnq  8771  mulpqnq  8774  fseq1p1m1  11077  injresinj  11155  seqfeq2  11301  seqres  11305  seqf1olem2  11318  hashgval  11576  hashinf  11578  hashgval2  11607  hashf1lem1  11659  seqcoll  11667  swrdccat1  11729  shftidt  11852  rlimres  12307  lo1res  12308  climres  12324  isercolllem3  12415  fsumss  12474  isumclim3  12498  fsum2dlem  12509  ackbijnn  12562  reeff1  12676  bitsf1  12913  sadcaddlem  12924  sadcadd  12925  sadadd2  12927  sadaddlem  12933  sadasslem  12937  sadeq  12939  eucalgcvga  13032  eucalg  13033  unbenlem  13231  strfv2d  13454  setsid  13463  setsnid  13464  funcres  14048  dmaf  14159  cdaf  14160  1stf1  14244  2ndf1  14247  1stfcl  14249  2ndfcl  14250  prf1st  14256  prf2nd  14257  1st2ndprf  14258  uncf2  14289  diag12  14296  diag2  14297  curf2ndf  14299  yonedalem22  14330  resmhm  14714  resghm  14977  efgsres  15325  efgredlemd  15331  efgredlem  15334  gsumzaddlem  15481  dprdfadd  15533  dprdres  15541  dmdprdsplitlem  15550  dprdcntz2  15551  dmdprdsplit2lem  15558  dprdsplit  15561  dpjidcl  15571  ablfac1eu  15586  mgpf  15630  prdscrngd  15674  abvres  15882  reslmhm  16083  ltbwe  16488  subrgascl  16513  subrgasclcl  16514  znf1o  16787  znunithash  16800  cnpresti  17306  cnprest  17307  lmres  17318  tx1cn  17594  tx2cn  17595  upxp  17608  uptx  17610  ptrescn  17624  txkgen  17637  cnmpt1st  17653  cnmpt2nd  17654  ptuncnv  17792  ptunhmeo  17793  cnextfres  18052  prdstmdd  18106  prdsxmslem2  18512  subgnm2  18628  remetdval  18773  rescncf  18880  lmle  19207  lmcau  19218  ovoliunlem1  19351  ovolicc2lem4  19369  mblvol  19379  mbflimsup  19511  limcdif  19716  limcres  19726  dvreslem  19749  dvres2lem  19750  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  c1lip1  19834  c1lip3  19836  dvgt0lem1  19839  dvivthlem1  19845  lhop1lem  19850  lhop  19853  dvcnvrelem1  19854  dvcvx  19857  ftc2ditglem  19882  itgsubstlem  19885  plyreres  20153  plyexmo  20183  aannenlem1  20198  taylthlem2  20243  ulmres  20257  ulmss  20266  psercn  20295  pserdvlem2  20297  reeff1o  20316  reefiso  20317  efcvx  20318  reefgim  20319  recosf1o  20390  resinf1o  20391  efif1olem4  20400  eff1olem  20403  relogcl  20426  eflog  20427  logef  20429  logeftb  20431  logltb  20447  logcn  20491  advlog  20498  advlogexp  20499  logtayl  20504  logccv  20507  dvcxp1  20579  cxpcn  20582  loglesqr  20595  asinrebnd  20694  dvatan  20728  leibpi  20735  efrlim  20761  jensen  20780  amgmlem  20781  wilthlem3  20806  ftalem3  20810  dvdsmulf1o  20932  fsumdvdsmul  20933  dchrelbas2  20974  dchrabs  20997  sum2dchr  21011  dchrisumlem1  21136  logdivsum  21180  log2sumbnd  21191  ostth2  21284  ostth  21286  redwlk  21559  eupares  21650  ghsubgolem  21911  sspnval  22189  hhssnv  22717  hhssmetdval  22731  ofresid  24008  xpinpreima  24257  xpinpreima2  24258  cnre2csqlem  24261  rmulccn  24267  zzsnm  24295  cnzh  24307  rezh  24308  measres  24529  cntmeas  24533  cntnevol  24535  1stmbfm  24563  2ndmbfm  24564  coinfliplem  24689  coinflipprob  24690  lgamgulmlem2  24767  lgamcvg2  24792  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem8  24837  txsconlem  24880  cvmfolem  24919  cvmliftmolem1  24921  cvmliftlem6  24930  cvmliftlem7  24931  cvmliftlem9  24933  fprodss  25227  fprodefsum  25251  fprod2dlem  25257  iprodclim3  25266  fvresval  25337  dfrdg2  25366  wfrlem4  25473  frrlem4  25498  sltres  25532  nodense  25557  funpartfv  25698  bpolylem  25998  itg2gt0cn  26159  areacirclem4  26183  areacirclem5  26185  filnetlem4  26300  eqfnun  26313  sdclem2  26336  caures  26356  ismtyres  26407  imaiinfv  26630  mzpcompact2lem  26698  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  jm2.27dlem1  26970  fnwe2lem2  27016  fnwe2lem3  27017  aomclem6  27024  deg1mhm  27394  hausgraph  27399  stoweidlem28  27644  afvres  27903  swrd0swrd  28009  bnj1379  28908  bnj1253  29092  bnj1280  29095  diaintclN  31541  dibintclN  31650  dihintcl  31827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-xp 4843  df-res 4849  df-iota 5377  df-fv 5421
  Copyright terms: Public domain W3C validator