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

Theorem fvres 5542
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 2791 . . . . 5  |-  x  e. 
_V
21brres 4961 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 873 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5240 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5263 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5263 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2340 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   class class class wbr 4023    |` cres 4691   iotacio 5217   ` cfv 5255
This theorem is referenced by:  funssfv  5543  fveqres  5560  feqresmpt  5576  dffv2  5592  fvreseq  5628  respreima  5654  ffvresb  5690  fnressn  5705  fressnfv  5707  fvresi  5711  fvunsn  5712  fvsnun1  5715  fvsnun2  5716  fsnunfv  5720  fnsuppres  5732  funfvima  5753  funiunfv  5774  soisores  5824  isores3  5832  isoini2  5836  f1oweALT  5851  ovres  5987  offres  6092  ofres  6094  fo1stres  6143  fo2ndres  6144  curry1  6210  curry2  6213  fparlem1  6218  fparlem2  6219  smores  6369  smores2  6371  tfrlem5  6396  tz7.44-2  6420  fr0g  6448  frsuc  6449  tz7.48lem  6453  seqomlem1  6462  seqomlem2  6463  seqomlem3  6464  seqomlem4  6465  onasuc  6527  onmsuc  6528  onesuc  6529  resixp  6851  fofinf1o  7137  ixpfi2  7154  ordtypelem4  7236  ordtypelem6  7238  ordtypelem7  7239  unxpwdom2  7302  cantnfres  7379  cantnfp1lem3  7382  dfac12lem1  7769  ackbij2lem2  7866  ackbij2lem3  7867  cfsmolem  7896  alephsing  7902  ttukeylem3  8138  fpwwe2lem6  8257  fpwwe2lem8  8259  fpwwe2lem9  8260  canthp1lem2  8275  inar1  8397  addpiord  8508  mulpiord  8509  addpqnq  8562  mulpqnq  8565  fseq1p1m1  10857  seqfeq2  11069  seqres  11073  seqf1olem2  11086  hashgval  11340  hashinf  11342  hashgval2  11360  hashf1lem1  11393  seqcoll  11401  swrdccat1  11460  shftidt  11577  rlimres  12032  lo1res  12033  climres  12049  isercolllem3  12140  fsumss  12198  isumclim3  12222  fsum2dlem  12233  ackbijnn  12286  reeff1  12400  bitsf1  12637  sadcaddlem  12648  sadcadd  12649  sadadd2  12651  sadaddlem  12657  sadasslem  12661  sadeq  12663  eucalgcvga  12756  eucalg  12757  unbenlem  12955  strfv2d  13178  setsid  13187  setsnid  13188  funcres  13770  dmaf  13881  cdaf  13882  1stf1  13966  2ndf1  13969  1stfcl  13971  2ndfcl  13972  prf1st  13978  prf2nd  13979  1st2ndprf  13980  uncf2  14011  diag12  14018  diag2  14019  curf2ndf  14021  yonedalem22  14052  resmhm  14436  resghm  14699  efgsres  15047  efgredlemd  15053  efgredlem  15056  gsumzaddlem  15203  dprdfadd  15255  dprdres  15263  dmdprdsplitlem  15272  dprdcntz2  15273  dmdprdsplit2lem  15280  dprdsplit  15283  dpjidcl  15293  ablfac1eu  15308  mgpf  15352  prdscrngd  15396  abvres  15604  reslmhm  15809  ltbwe  16214  subrgascl  16239  subrgasclcl  16240  znf1o  16505  znunithash  16518  cnpresti  17016  cnprest  17017  lmres  17028  tx1cn  17303  tx2cn  17304  upxp  17317  uptx  17319  ptrescn  17333  txkgen  17346  cnmpt1st  17362  cnmpt2nd  17363  ptuncnv  17498  ptunhmeo  17499  prdstmdd  17806  prdsxmslem2  18075  subgnm2  18150  remetdval  18295  rescncf  18401  lmle  18727  lmcau  18738  ovoliunlem1  18861  ovolicc2lem4  18879  mblvol  18889  mbflimsup  19021  limcdif  19226  limcres  19236  dvreslem  19259  dvres2lem  19260  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  c1lip1  19344  c1lip3  19346  dvgt0lem1  19349  dvivthlem1  19355  lhop1lem  19360  lhop  19363  dvcnvrelem1  19364  dvcvx  19367  ftc2ditglem  19392  itgsubstlem  19395  plyreres  19663  plyexmo  19693  aannenlem1  19708  taylthlem2  19753  ulmres  19767  ulmss  19774  psercn  19802  pserdvlem2  19804  reeff1o  19823  reefiso  19824  efcvx  19825  reefgim  19826  recosf1o  19897  resinf1o  19898  efif1olem4  19907  eff1olem  19910  relogcl  19932  eflog  19933  logef  19935  logeftb  19937  logltb  19953  logcn  19994  advlog  20001  advlogexp  20002  logtayl  20007  logccv  20010  dvcxp1  20082  cxpcn  20085  loglesqr  20098  asinrebnd  20197  dvatan  20231  leibpi  20238  efrlim  20264  jensen  20283  amgmlem  20284  wilthlem3  20308  ftalem3  20312  dvdsmulf1o  20434  fsumdvdsmul  20435  dchrelbas2  20476  dchrabs  20499  sum2dchr  20513  dchrisumlem1  20638  logdivsum  20682  log2sumbnd  20693  ostth2  20786  ostth  20788  ghsubgolem  21037  sspnval  21313  hhssnv  21841  hhssmetdval  21855  cntnevol  23175  xpinpreima  23290  xpinpreima2  23291  cnre2csqlem  23294  rmulccn  23301  measres  23549  cntmeas  23553  1stmbfm  23565  2ndmbfm  23566  coinfliplem  23679  coinflipprob  23680  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem8  23729  txsconlem  23771  cvmfolem  23810  cvmliftmolem1  23812  cvmliftlem6  23821  cvmliftlem7  23822  cvmliftlem9  23824  eupares  23899  fvresval  24123  dfrdg2  24152  wfrlem4  24259  frrlem4  24284  sltres  24318  nodense  24343  funpartfv  24483  bpolylem  24783  areacirclem4  24927  areacirclem5  24929  oprssopvg  25034  eqfnung2  25118  prl2  25169  idsubfun  25858  vtare  25885  vtarsu  25886  vtarl  25887  filnetlem4  26330  eqfnun  26387  sdclem2  26452  caures  26476  ismtyres  26532  imaiinfv  26759  mzpcompact2lem  26829  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  jm2.27dlem1  27102  fnwe2lem2  27148  fnwe2lem3  27149  aomclem6  27156  deg1mhm  27526  hausgraph  27531  stoweidlem28  27777  afvres  28034  bnj1379  28863  bnj1253  29047  bnj1280  29050  diaintclN  31248  dibintclN  31357  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4695  df-res 4701  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator