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

Theorem fvres 5699
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 2970 . . . . 5  |-  x  e. 
_V
21brres 5112 . . . 4  |-  ( A ( F  |`  B ) x  <->  ( A F x  /\  A  e.  B ) )
32rbaib 898 . . 3  |-  ( A  e.  B  ->  ( A ( F  |`  B ) x  <->  A F x ) )
43iotabidv 5397 . 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 2495 1  |-  ( A  e.  B  ->  (
( F  |`  B ) `
 A )  =  ( F `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   class class class wbr 4287    |` cres 4837   iotacio 5374   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-xp 4841  df-res 4847  df-iota 5376  df-fv 5421
This theorem is referenced by:  funssfv  5700  fveqres  5719  feqresmpt  5740  dffv2  5759  fvreseq0  5798  respreima  5827  ffvresb  5869  fnressn  5889  fressnfv  5891  fvresi  5899  fvunsn  5905  fvsnun1  5908  fvsnun2  5909  fsnunfv  5913  fnsuppresOLD  5933  funfvima  5947  funiunfv  5960  soisores  6013  isores3  6021  isoini2  6025  ovres  6225  ofres  6330  f1oweALT  6556  offres  6567  fo1stres  6595  fo2ndres  6596  curry1  6659  curry2  6662  fparlem1  6667  fparlem2  6668  fo2ndf  6674  f1o2ndf1  6675  fnsuppres  6711  smores  6805  smores2  6807  tfrlem1  6827  tz7.44-2  6855  fr0g  6883  frsuc  6884  tz7.48lem  6888  seqomlem1  6897  seqomlem2  6898  seqomlem3  6899  seqomlem4  6900  onasuc  6960  onmsuc  6961  onesuc  6962  resixp  7290  fofinf1o  7584  ixpfi2  7601  ordtypelem4  7727  ordtypelem6  7729  ordtypelem7  7730  unxpwdom2  7795  cantnfres  7877  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  dfac12lem1  8304  ackbij2lem2  8401  ackbij2lem3  8402  cfsmolem  8431  alephsing  8437  ttukeylem3  8672  fpwwe2lem6  8794  fpwwe2lem8  8796  fpwwe2lem9  8797  canthp1lem2  8812  inar1  8934  addpiord  9045  mulpiord  9046  addpqnq  9099  mulpqnq  9102  fseq1p1m1  11526  injresinj  11631  seqfeq2  11821  seqres  11825  seqf1olem2  11838  hashgval  12098  hashinf  12100  hashgval2  12133  hashf1lem1  12200  seqcoll  12208  swrdccat1  12343  shftidt  12563  rlimres  13028  lo1res  13029  climres  13045  isercolllem3  13136  fsumss  13194  isumclim3  13218  fsum2dlem  13229  ackbijnn  13283  reeff1  13396  bitsf1  13634  sadcaddlem  13645  sadcadd  13646  sadadd2  13648  sadaddlem  13654  sadasslem  13658  sadeq  13660  eucalgcvga  13753  eucalg  13754  unbenlem  13961  strfv2d  14198  setsid  14207  setsnid  14208  funcres  14798  dmaf  14909  cdaf  14910  1stf1  14994  2ndf1  14997  1stfcl  14999  2ndfcl  15000  prf1st  15006  prf2nd  15007  1st2ndprf  15008  uncf2  15039  diag12  15046  diag2  15047  curf2ndf  15049  yonedalem22  15080  lubval  15146  glbval  15159  resmhm  15478  resghm  15754  efgsres  16226  efgredlemd  16232  efgredlem  16235  gsumzaddlem  16399  gsumzaddlemOLD  16401  dprdfadd  16498  dprdfaddOLD  16505  dprdres  16513  dmdprdsplitlem  16522  dmdprdsplitlemOLD  16523  dprdcntz2  16524  dmdprdsplit2lem  16532  dprdsplit  16535  dpjidcl  16545  dpjidclOLD  16552  ablfac1eu  16562  mgpf  16644  prdscrngd  16693  abvres  16902  reslmhm  17110  ltbwe  17529  subrgascl  17555  subrgasclcl  17556  znf1o  17959  znunithash  17972  psgndiflemB  18005  smadiadetlem3  18449  cnpresti  18867  cnprest  18868  lmres  18879  tx1cn  19157  tx2cn  19158  upxp  19171  uptx  19173  ptrescn  19187  txkgen  19200  cnmpt1st  19216  cnmpt2nd  19217  ptuncnv  19355  ptunhmeo  19356  cnextfres  19615  prdstmdd  19669  prdsxmslem2  20079  subgnm2  20195  remetdval  20341  rescncf  20448  lmle  20787  lmcau  20798  ovoliunlem1  20960  ovolicc2lem4  20978  mblvol  20988  mbflimsup  21119  limcdif  21326  limcres  21336  dvreslem  21359  dvres2lem  21360  dvlip  21440  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  c1lip1  21444  c1lip3  21446  dvgt0lem1  21449  dvivthlem1  21455  lhop1lem  21460  lhop  21463  dvcnvrelem1  21464  dvcvx  21467  ftc2ditglem  21492  itgsubstlem  21495  plyreres  21724  plyexmo  21754  aannenlem1  21769  taylthlem2  21814  ulmres  21828  ulmss  21837  psercn  21866  pserdvlem2  21868  reeff1o  21887  reefiso  21888  efcvx  21889  reefgim  21890  recosf1o  21966  resinf1o  21967  efif1olem4  21976  eff1olem  21979  relogcl  22002  eflog  22003  logef  22005  logeftb  22007  logltb  22023  logcn  22067  advlog  22074  advlogexp  22075  logtayl  22080  logccv  22083  dvcxp1  22155  cxpcn  22158  loglesqr  22171  asinrebnd  22271  dvatan  22305  leibpi  22312  efrlim  22338  jensen  22357  amgmlem  22358  wilthlem3  22383  ftalem3  22387  dvdsmulf1o  22509  fsumdvdsmul  22510  dchrelbas2  22551  dchrabs  22574  sum2dchr  22588  dchrisumlem1  22713  logdivsum  22757  log2sumbnd  22768  ostth2  22861  ostth  22863  redwlk  23456  eupares  23547  ghsubgolem  23808  sspnval  24086  hhssnv  24616  hhssmetdval  24630  ofresid  25911  xpinpreima  26288  xpinpreima2  26289  cnre2csqlem  26292  rmulccn  26310  zzsnm  26341  zzsnmOLD  26342  cnzh  26351  rezh  26352  measres  26588  cntmeas  26592  cntnevol  26594  1stmbfm  26627  2ndmbfm  26628  eulerpartgbij  26707  eulerpartlemgvv  26711  eulerpartlemgs2  26715  iwrdsplit  26722  fibp1  26736  coinfliplem  26813  coinflipprob  26814  gsumnunsn  26889  plyrecld  26902  signstres  26928  lgamgulmlem2  26968  lgamcvg2  26993  subfacp1lem3  27022  subfacp1lem5  27024  erdszelem8  27038  txsconlem  27081  cvmfolem  27120  cvmliftmolem1  27122  cvmliftlem6  27131  cvmliftlem7  27132  cvmliftlem9  27134  fprodss  27412  fprodefsum  27436  fprod2dlem  27442  iprodclim3  27451  fvresval  27529  dfrdg2  27560  wfrlem4  27678  frrlem4  27722  sltres  27756  nodense  27781  funpartfv  27927  bpolylem  28142  finixpnum  28367  itg2gt0cn  28400  dvcncxp1  28430  areacirclem2  28438  areacirclem4  28440  filnetlem4  28555  eqfnun  28568  sdclem2  28591  caures  28609  ismtyres  28660  imaiinfv  28982  mzpcompact2lem  29041  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  jm2.27dlem1  29311  fnwe2lem2  29357  fnwe2lem3  29358  aomclem6  29365  deg1mhm  29528  hausgraph  29533  stoweidlem28  29776  afvres  30031  fvressn  30105  lincdifsn  30847  lindslinindimp2lem4  30884  lindslinindsimp2lem5  30885  lincresunit3lem2  30903  bnj1379  31711  bnj1253  31895  bnj1280  31898  diaintclN  34543  dibintclN  34652  dihintcl  34829
  Copyright terms: Public domain W3C validator