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

Theorem fvres 5686
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 2903 . . . . 5  |-  x  e. 
_V
21brres 5093 . . . 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 5380 . 2  |-  ( A  e.  B  ->  ( iota x A ( F  |`  B ) x )  =  ( iota x A F x ) )
5 df-fv 5403 . 2  |-  ( ( F  |`  B ) `  A )  =  ( iota x A ( F  |`  B )
x )
6 df-fv 5403 . 2  |-  ( F `
 A )  =  ( iota x A F x )
74, 5, 63eqtr4g 2445 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   class class class wbr 4154    |` cres 4821   iotacio 5357   ` cfv 5395
This theorem is referenced by:  funssfv  5687  fveqres  5704  feqresmpt  5720  dffv2  5736  fvreseq  5773  respreima  5799  ffvresb  5840  fnressn  5858  fressnfv  5860  fvresi  5864  fvunsn  5865  fvsnun1  5868  fvsnun2  5869  fsnunfv  5873  fnsuppres  5892  funfvima  5913  funiunfv  5935  soisores  5987  isores3  5995  isoini2  5999  f1oweALT  6014  ovres  6153  offres  6259  ofres  6261  fo1stres  6310  fo2ndres  6311  curry1  6378  curry2  6381  fparlem1  6386  fparlem2  6387  smores  6551  smores2  6553  tfrlem5  6578  tz7.44-2  6602  fr0g  6630  frsuc  6631  tz7.48lem  6635  seqomlem1  6644  seqomlem2  6645  seqomlem3  6646  seqomlem4  6647  onasuc  6709  onmsuc  6710  onesuc  6711  resixp  7034  fofinf1o  7324  ixpfi2  7341  ordtypelem4  7424  ordtypelem6  7426  ordtypelem7  7427  unxpwdom2  7490  cantnfres  7567  cantnfp1lem3  7570  dfac12lem1  7957  ackbij2lem2  8054  ackbij2lem3  8055  cfsmolem  8084  alephsing  8090  ttukeylem3  8325  fpwwe2lem6  8444  fpwwe2lem8  8446  fpwwe2lem9  8447  canthp1lem2  8462  inar1  8584  addpiord  8695  mulpiord  8696  addpqnq  8749  mulpqnq  8752  fseq1p1m1  11053  injresinj  11128  seqfeq2  11274  seqres  11278  seqf1olem2  11291  hashgval  11549  hashinf  11551  hashgval2  11580  hashf1lem1  11632  seqcoll  11640  swrdccat1  11702  shftidt  11825  rlimres  12280  lo1res  12281  climres  12297  isercolllem3  12388  fsumss  12447  isumclim3  12471  fsum2dlem  12482  ackbijnn  12535  reeff1  12649  bitsf1  12886  sadcaddlem  12897  sadcadd  12898  sadadd2  12900  sadaddlem  12906  sadasslem  12910  sadeq  12912  eucalgcvga  13005  eucalg  13006  unbenlem  13204  strfv2d  13427  setsid  13436  setsnid  13437  funcres  14021  dmaf  14132  cdaf  14133  1stf1  14217  2ndf1  14220  1stfcl  14222  2ndfcl  14223  prf1st  14229  prf2nd  14230  1st2ndprf  14231  uncf2  14262  diag12  14269  diag2  14270  curf2ndf  14272  yonedalem22  14303  resmhm  14687  resghm  14950  efgsres  15298  efgredlemd  15304  efgredlem  15307  gsumzaddlem  15454  dprdfadd  15506  dprdres  15514  dmdprdsplitlem  15523  dprdcntz2  15524  dmdprdsplit2lem  15531  dprdsplit  15534  dpjidcl  15544  ablfac1eu  15559  mgpf  15603  prdscrngd  15647  abvres  15855  reslmhm  16056  ltbwe  16461  subrgascl  16486  subrgasclcl  16487  znf1o  16756  znunithash  16769  cnpresti  17275  cnprest  17276  lmres  17287  tx1cn  17563  tx2cn  17564  upxp  17577  uptx  17579  ptrescn  17593  txkgen  17606  cnmpt1st  17622  cnmpt2nd  17623  ptuncnv  17761  ptunhmeo  17762  cnextfres  18021  prdstmdd  18075  prdsxmslem2  18450  subgnm2  18547  remetdval  18692  rescncf  18799  lmle  19126  lmcau  19137  ovoliunlem1  19266  ovolicc2lem4  19284  mblvol  19294  mbflimsup  19426  limcdif  19631  limcres  19641  dvreslem  19664  dvres2lem  19665  dvlip  19745  dvlipcn  19746  dvlip2  19747  c1liplem1  19748  c1lip1  19749  c1lip3  19751  dvgt0lem1  19754  dvivthlem1  19760  lhop1lem  19765  lhop  19768  dvcnvrelem1  19769  dvcvx  19772  ftc2ditglem  19797  itgsubstlem  19800  plyreres  20068  plyexmo  20098  aannenlem1  20113  taylthlem2  20158  ulmres  20172  ulmss  20181  psercn  20210  pserdvlem2  20212  reeff1o  20231  reefiso  20232  efcvx  20233  reefgim  20234  recosf1o  20305  resinf1o  20306  efif1olem4  20315  eff1olem  20318  relogcl  20341  eflog  20342  logef  20344  logeftb  20346  logltb  20362  logcn  20406  advlog  20413  advlogexp  20414  logtayl  20419  logccv  20422  dvcxp1  20494  cxpcn  20497  loglesqr  20510  asinrebnd  20609  dvatan  20643  leibpi  20650  efrlim  20676  jensen  20695  amgmlem  20696  wilthlem3  20721  ftalem3  20725  dvdsmulf1o  20847  fsumdvdsmul  20848  dchrelbas2  20889  dchrabs  20912  sum2dchr  20926  dchrisumlem1  21051  logdivsum  21095  log2sumbnd  21106  ostth2  21199  ostth  21201  redwlk  21455  eupares  21546  ghsubgolem  21807  sspnval  22085  hhssnv  22613  hhssmetdval  22627  xpinpreima  24109  xpinpreima2  24110  cnre2csqlem  24113  rmulccn  24119  zzsnm  24145  rrhre  24184  measres  24371  cntmeas  24375  cntnevol  24377  1stmbfm  24405  2ndmbfm  24406  coinfliplem  24516  coinflipprob  24517  lgamgulmlem2  24594  lgamcvg2  24619  subfacp1lem3  24648  subfacp1lem5  24650  erdszelem8  24664  txsconlem  24707  cvmfolem  24746  cvmliftmolem1  24748  cvmliftlem6  24757  cvmliftlem7  24758  cvmliftlem9  24760  fprodss  25054  fprodefsum  25078  iprodclim3  25086  fvresval  25148  dfrdg2  25177  wfrlem4  25284  frrlem4  25309  sltres  25343  nodense  25368  funpartfv  25509  bpolylem  25809  itg2gt0cn  25961  areacirclem4  25985  areacirclem5  25987  filnetlem4  26102  eqfnun  26115  sdclem2  26138  caures  26158  ismtyres  26209  imaiinfv  26432  mzpcompact2lem  26500  2rexfrabdioph  26548  3rexfrabdioph  26549  4rexfrabdioph  26550  6rexfrabdioph  26551  7rexfrabdioph  26552  jm2.27dlem1  26772  fnwe2lem2  26818  fnwe2lem3  26819  aomclem6  26826  deg1mhm  27196  hausgraph  27201  stoweidlem28  27446  afvres  27706  bnj1379  28541  bnj1253  28725  bnj1280  28728  diaintclN  31174  dibintclN  31283  dihintcl  31460
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 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pr 4345
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-opab 4209  df-xp 4825  df-res 4831  df-iota 5359  df-fv 5403
  Copyright terms: Public domain W3C validator