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

Theorem fvres 5885
Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fvres

Proof of Theorem fvres
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vex 3112 . . . . 5
21brres 5285 . . . 4
32rbaib 906 . . 3
43iotabidv 5577 . 2
5 df-fv 5601 . 2
6 df-fv 5601 . 2
74, 5, 63eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   class class class wbr 4452  |`cres 5006  iotacio 5554  `cfv 5593
This theorem is referenced by:  funssfv  5886  fveqres  5905  feqresmpt  5927  dffv2  5946  fvreseq0  5987  respreima  6016  fveqressseq  6027  ffvresb  6062  fnressn  6083  fressnfv  6085  fvressn  6087  fvresi  6097  fvsnun1  6106  fvsnun2  6107  fsnunfv  6111  fnsuppresOLD  6131  funfvima  6147  funiunfv  6160  soisores  6223  isores3  6231  isoini2  6235  ovres  6442  ofres  6555  f1oweALT  6784  offres  6795  fo1stres  6824  fo2ndres  6825  curry1  6892  curry2  6895  fparlem1  6900  fparlem2  6901  fo2ndf  6907  f1o2ndf1  6908  fnsuppres  6946  smores  7042  smores2  7044  tfrlem1  7064  tz7.44-2  7092  fr0g  7120  frsuc  7121  tz7.48lem  7125  seqomlem1  7134  seqomlem2  7135  seqomlem3  7136  seqomlem4  7137  onasuc  7197  onmsuc  7198  onesuc  7199  resixp  7524  fofinf1o  7821  ixpfi2  7838  ordtypelem4  7967  ordtypelem6  7969  ordtypelem7  7970  unxpwdom2  8035  cantnfres  8117  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  dfac12lem1  8544  ackbij2lem2  8641  ackbij2lem3  8642  cfsmolem  8671  alephsing  8677  ttukeylem3  8912  fpwwe2lem6  9034  fpwwe2lem8  9036  fpwwe2lem9  9037  canthp1lem2  9052  inar1  9174  addpiord  9283  mulpiord  9284  addpqnq  9337  mulpqnq  9340  fseq1p1m1  11781  injresinj  11926  seqfeq2  12130  seqres  12134  seqf1olem2  12147  hashgval  12408  hashinf  12410  hashgval2  12446  hashf1lem1  12504  seqcoll  12512  swrdccat1  12682  shftidt  12915  rlimres  13381  lo1res  13382  climres  13398  isercolllem3  13489  fsumss  13547  isumclim3  13574  fsum2dlem  13585  ackbijnn  13640  fprodss  13755  fprod2dlem  13784  iprodclim3  13793  fprodefsum  13830  reeff1  13855  bitsf1  14096  sadcaddlem  14107  sadcadd  14108  sadadd2  14110  sadaddlem  14116  sadasslem  14120  sadeq  14122  eucalgcvga  14215  eucalg  14216  unbenlem  14426  strfv2d  14664  setsid  14673  setsnid  14674  funcres  15265  dmaf  15376  cdaf  15377  1stf1  15461  2ndf1  15464  1stfcl  15466  2ndfcl  15467  prf1st  15473  prf2nd  15474  1st2ndprf  15475  uncf2  15506  diag12  15513  diag2  15514  curf2ndf  15516  yonedalem22  15547  lubval  15614  glbval  15627  resmhm  15990  resghm  16283  efgsres  16756  efgredlemd  16762  efgredlem  16765  gsumzaddlem  16934  gsumzaddlemOLD  16936  dprdfadd  17060  dprdfaddOLD  17067  dprdres  17075  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  dprdcntz2  17086  dmdprdsplit2lem  17094  dprdsplit  17097  dpjidcl  17107  dpjidclOLD  17114  ablfac1eu  17124  mgpf  17210  prdscrngd  17262  abvres  17488  reslmhm  17698  ltbwe  18137  subrgascl  18163  subrgasclcl  18164  znf1o  18590  znunithash  18603  psgndiflemB  18636  smadiadetlem3  19170  cnpresti  19789  cnprest  19790  lmres  19801  tx1cn  20110  tx2cn  20111  upxp  20124  uptx  20126  ptrescn  20140  txkgen  20153  cnmpt1st  20169  cnmpt2nd  20170  ptuncnv  20308  ptunhmeo  20309  cnextfres  20568  prdstmdd  20622  prdsxmslem2  21032  subgnm2  21148  remetdval  21294  rescncf  21401  lmle  21740  lmcau  21751  ovoliunlem1  21913  ovolicc2lem4  21931  mblvol  21941  mbflimsup  22073  limcdif  22280  limcres  22290  dvreslem  22313  dvres2lem  22314  dvlip  22394  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  c1lip1  22398  c1lip3  22400  dvgt0lem1  22403  dvivthlem1  22409  lhop1lem  22414  lhop  22417  dvcnvrelem1  22418  dvcvx  22421  ftc2ditglem  22446  itgsubstlem  22449  plyreres  22679  plyexmo  22709  aannenlem1  22724  taylthlem2  22769  ulmres  22783  ulmss  22792  psercn  22821  pserdvlem2  22823  reeff1o  22842  reefiso  22843  efcvx  22844  reefgim  22845  recosf1o  22922  resinf1o  22923  efif1olem4  22932  eff1olem  22935  relogcl  22963  eflog  22964  logef  22966  logeftb  22968  logltb  22984  logcn  23028  advlog  23035  advlogexp  23036  logtayl  23041  logccv  23044  dvcxp1  23116  cxpcn  23119  loglesqrt  23132  asinrebnd  23232  dvatan  23266  leibpi  23273  efrlim  23299  jensen  23318  amgmlem  23319  wilthlem3  23344  ftalem3  23348  dvdsmulf1o  23470  fsumdvdsmul  23471  dchrelbas2  23512  dchrabs  23535  sum2dchr  23549  dchrisumlem1  23674  logdivsum  23718  log2sumbnd  23729  ostth2  23822  ostth  23824  redwlk  24608  eupares  24975  ghsubgolemOLD  25372  sspnval  25650  hhssnv  26180  hhssmetdval  26194  foresf1o  27403  ofresid  27482  xpinpreima  27888  xpinpreima2  27889  cnre2csqlem  27892  rmulccn  27910  zzsnm  27941  zzsnmOLD  27942  cnzh  27951  rezh  27952  measres  28193  cntmeas  28197  cntnevol  28199  1stmbfm  28231  2ndmbfm  28232  eulerpartgbij  28311  eulerpartlemgvv  28315  eulerpartlemgs2  28319  iwrdsplit  28326  fibp1  28340  coinfliplem  28417  coinflipprob  28418  gsumnunsn  28493  plyrecld  28506  signstres  28532  lgamgulmlem2  28572  lgamcvg2  28597  subfacp1lem3  28626  subfacp1lem5  28628  erdszelem8  28642  txsconlem  28685  cvmfolem  28724  cvmliftmolem1  28726  cvmliftlem6  28735  cvmliftlem7  28736  cvmliftlem9  28738  mrsubff1  28874  msubff1  28916  fvresval  29197  dfrdg2  29228  wfrlem4  29346  frrlem4  29390  sltres  29424  nodense  29449  funpartfv  29595  bpolylem  29810  finixpnum  30038  itg2gt0cn  30070  dvcncxp1  30100  areacirclem2  30108  areacirclem4  30110  filnetlem4  30199  eqfnun  30212  sdclem2  30235  caures  30253  ismtyres  30304  imaiinfv  30625  mzpcompact2lem  30684  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  jm2.27dlem1  30951  fnwe2lem2  30997  fnwe2lem3  30998  aomclem6  31005  deg1mhm  31167  hausgraph  31172  radcnvrat  31195  mccllem  31605  limcperiod  31634  limcleqr  31650  limclner  31657  resincncf  31677  cncfperiod  31681  icccncfext  31690  cncfiooicclem1  31696  dvbdfbdioolem1  31725  dvnprodlem1  31743  dvnprodlem2  31744  itgioocnicc  31776  stoweidlem28  31810  fourierdlem18  31907  fourierdlem40  31929  fourierdlem42  31931  fourierdlem46  31935  fourierdlem51  31940  fourierdlem70  31959  fourierdlem71  31960  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem80  31969  fourierdlem81  31970  fourierdlem82  31971  fourierdlem84  31973  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem93  31982  fourierdlem94  31983  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  afvres  32257  resmgmhm  32486  rhmsubclem2  32895  rhmsubcOLDlem2  32914  lincdifsn  33025  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  lincresunit3lem2  33081  bnj1379  33889  bnj1253  34073  bnj1280  34076  diaintclN  36785  dibintclN  36894  dihintcl  37071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-res 5016  df-iota 5556  df-fv 5601
  Copyright terms: Public domain W3C validator