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

Theorem fvres 6194
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 3198 . . . . 5 𝑥 ∈ V
21brres 5391 . . . 4 (𝐴(𝐹𝐵)𝑥 ↔ (𝐴𝐹𝑥𝐴𝐵))
32rbaib 946 . . 3 (𝐴𝐵 → (𝐴(𝐹𝐵)𝑥𝐴𝐹𝑥))
43iotabidv 5860 . 2 (𝐴𝐵 → (℩𝑥𝐴(𝐹𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5 df-fv 5884 . 2 ((𝐹𝐵)‘𝐴) = (℩𝑥𝐴(𝐹𝐵)𝑥)
6 df-fv 5884 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
74, 5, 63eqtr4g 2679 1 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988   class class class wbr 4644  cres 5106  cio 5837  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-xp 5110  df-res 5116  df-iota 5839  df-fv 5884
This theorem is referenced by:  fvresd  6195  funssfv  6196  fveqres  6217  feqresmpt  6237  dffv2  6258  fvreseq0  6303  respreima  6330  fveqressseq  6341  ffvresb  6380  fnressn  6410  fressnfv  6412  fvressn  6414  fvresi  6424  fvsnun1  6433  fvsnun2  6434  fsnunfv  6438  funfvima  6477  resfvresima  6479  funiunfv  6491  soisores  6562  isores3  6570  isoini2  6574  ovres  6785  ofres  6898  f1oweALT  7137  offres  7148  fo1stres  7177  fo2ndres  7178  curry1  7254  curry2  7257  fparlem1  7262  fparlem2  7263  fo2ndf  7269  f1o2ndf1  7270  fnsuppres  7307  wfrlem4  7403  smores  7434  smores2  7436  tfrlem1  7457  tz7.44-2  7488  fr0g  7516  frsuc  7517  tz7.48lem  7521  seqomlem1  7530  seqomlem2  7531  seqomlem3  7532  seqomlem4  7533  onasuc  7593  onmsuc  7594  onesuc  7595  resixp  7928  fofinf1o  8226  ixpfi2  8249  ordtypelem4  8411  ordtypelem6  8413  ordtypelem7  8414  unxpwdom2  8478  cantnfres  8559  cantnfp1lem3  8562  dfac12lem1  8950  ackbij2lem2  9047  ackbij2lem3  9048  cfsmolem  9077  alephsing  9083  ttukeylem3  9318  fpwwe2lem6  9442  fpwwe2lem8  9444  fpwwe2lem9  9445  canthp1lem2  9460  inar1  9582  addpiord  9691  mulpiord  9692  addpqnq  9745  mulpqnq  9748  fseq1p1m1  12398  injresinj  12572  seqfeq2  12807  seqres  12811  seqf1olem2  12824  hashgval  13103  hashinf  13105  hashgval2  13150  hashf1lem1  13222  seqcoll  13231  swrdccat1  13439  shftidt  13803  rlimres  14270  lo1res  14271  climres  14287  isercolllem3  14378  fsumss  14437  isumclim3  14471  fsum2dlem  14482  ackbijnn  14541  fprodss  14659  fprod2dlem  14691  iprodclim3  14712  bpolylem  14760  fprodefsum  14806  reeff1  14831  bitsf1  15149  sadcaddlem  15160  sadcadd  15161  sadadd2  15163  sadaddlem  15169  sadasslem  15173  sadeq  15175  eucalgcvga  15280  eucalg  15281  unbenlem  15593  strfv2d  15886  setsid  15895  setsnid  15896  funcres  16537  dmaf  16680  cdaf  16681  1stf1  16813  2ndf1  16816  1stfcl  16818  2ndfcl  16819  prf1st  16825  prf2nd  16826  1st2ndprf  16827  uncf2  16858  diag12  16865  diag2  16866  curf2ndf  16868  yonedalem22  16899  lubval  16965  glbval  16978  resmhm  17340  resghm  17657  efgsres  18132  efgredlemd  18138  efgredlem  18141  gsumzaddlem  18302  dprdfadd  18400  dprdres  18408  dmdprdsplitlem  18417  dprdcntz2  18418  dmdprdsplit2lem  18425  dprdsplit  18428  dpjidcl  18438  ablfac1eu  18453  mgpf  18540  prdscrngd  18594  abvres  18820  reslmhm  19033  ltbwe  19453  subrgascl  19479  subrgasclcl  19480  znf1o  19881  znunithash  19894  psgndiflemB  19927  smadiadetlem3  20455  cnpresti  21073  cnprest  21074  lmres  21085  tx1cn  21393  tx2cn  21394  upxp  21407  uptx  21409  ptrescn  21423  cnmpt1st  21452  cnmpt2nd  21453  ptuncnv  21591  ptunhmeo  21592  cnextfres1  21853  prdstmdd  21908  prdsxmslem2  22315  subgnm2  22419  remetdval  22573  rescncf  22681  isncvsngp  22930  lmle  23080  lmcau  23092  ovoliunlem1  23251  ovolicc2lem4  23269  mblvol  23279  mbflimsup  23414  limcdif  23621  limcres  23631  dvreslem  23654  dvres2lem  23655  dvlip  23737  dvlipcn  23738  dvlip2  23739  c1liplem1  23740  c1lip1  23741  c1lip3  23743  dvgt0lem1  23746  dvivthlem1  23752  lhop1lem  23757  lhop  23760  dvcnvrelem1  23761  dvcvx  23764  ftc2ditglem  23789  itgsubstlem  23792  plyreres  24019  plyexmo  24049  aannenlem1  24064  taylthlem2  24109  ulmres  24123  ulmss  24132  psercn  24161  pserdvlem2  24163  reeff1o  24182  reefiso  24183  efcvx  24184  reefgim  24185  recosf1o  24262  resinf1o  24263  efif1olem4  24272  eff1olem  24275  relogcl  24303  eflog  24304  logef  24309  logeftb  24311  logltb  24327  logcn  24374  advlog  24381  advlogexp  24382  logtayl  24387  logccv  24390  dvcxp1  24462  dvcncxp1  24465  cxpcn  24467  loglesqrt  24480  asinrebnd  24609  dvatan  24643  leibpi  24650  efrlim  24677  jensen  24696  amgmlem  24697  lgamgulmlem2  24737  lgamcvg2  24762  wilthlem3  24777  ftalem3  24782  dvdsmulf1o  24901  fsumdvdsmul  24902  dchrelbas2  24943  dchrabs  24966  sum2dchr  24980  dchrisumlem1  25159  logdivsum  25203  log2sumbnd  25214  ostth2  25307  ostth  25309  vtxdginducedm1lem3  26418  wlkres  26548  redwlk  26550  pthdivtx  26606  pthdlem1  26643  sspnval  27562  hhssnv  28091  hhssmetdval  28105  foresf1o  29315  ofresid  29417  1stpreimas  29457  xpinpreima  29926  xpinpreima2  29927  cnre2csqlem  29930  rmulccn  29948  zzsnm  29979  cnzh  29988  rezh  29989  measres  30259  cntmeas  30263  cntnevol  30265  1stmbfm  30296  2ndmbfm  30297  carsggect  30354  omsmeas  30359  eulerpartgbij  30408  eulerpartlemgvv  30412  eulerpartlemgs2  30416  iwrdsplit  30423  fibp1  30437  coinfliplem  30514  coinflipprob  30515  gsumnunsn  30589  plyrecld  30600  signstres  30626  ftc2re  30650  bnj1379  30875  bnj1253  31059  bnj1280  31062  subfacp1lem3  31138  subfacp1lem5  31140  erdszelem8  31154  txsconnlem  31196  cvmfolem  31235  cvmliftmolem1  31237  cvmliftlem6  31246  cvmliftlem7  31247  cvmliftlem9  31249  mrsubff1  31385  msubff1  31427  fvresval  31641  dfrdg2  31675  frrlem4  31757  sltres  31789  nodense  31816  nolt02o  31819  funpartfv  32027  filnetlem4  32351  icoreunrn  33178  finixpnum  33365  poimirlem3  33383  poimirlem4  33384  poimirlem8  33388  poimirlem26  33406  poimirlem27  33407  itg2gt0cn  33436  areacirclem2  33472  areacirclem4  33474  eqfnun  33487  sdclem2  33509  caures  33527  ismtyres  33578  diaintclN  36166  dibintclN  36275  dihintcl  36452  imaiinfv  37075  mzpcompact2lem  37133  2rexfrabdioph  37179  3rexfrabdioph  37180  4rexfrabdioph  37181  6rexfrabdioph  37182  7rexfrabdioph  37183  jm2.27dlem1  37395  fnwe2lem2  37440  fnwe2lem3  37441  aomclem6  37448  deg1mhm  37604  hausgraph  37609  radcnvrat  38333  wessf1ornlem  39187  feqresmptf  39249  mccllem  39629  limcperiod  39660  limcleqr  39676  limclner  39683  limsupvaluz2  39770  supcnvlimsup  39772  limsupgtlem  39803  resincncf  39851  cncfperiod  39855  icccncfext  39863  cncfiooicclem1  39869  dvbdfbdioolem1  39906  dvnprodlem1  39924  dvnprodlem2  39925  itgioocnicc  39956  stoweidlem28  40008  fourierdlem18  40105  fourierdlem40  40127  fourierdlem42  40129  fourierdlem46  40132  fourierdlem51  40137  fourierdlem70  40156  fourierdlem71  40157  fourierdlem73  40159  fourierdlem74  40160  fourierdlem75  40161  fourierdlem76  40162  fourierdlem78  40164  fourierdlem80  40166  fourierdlem81  40167  fourierdlem82  40168  fourierdlem84  40170  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem92  40178  fourierdlem93  40179  fourierdlem94  40180  fourierdlem101  40187  fourierdlem103  40189  fourierdlem104  40190  fourierdlem111  40197  fourierdlem112  40198  fourierdlem113  40199  sge0tsms  40360  sge0f1o  40362  sge0sup  40371  sge0less  40372  sge0ltfirp  40380  sge0resrnlem  40383  sge0resplit  40386  sge0le  40387  sge0split  40389  sge0fodjrnlem  40396  sge0iun  40399  meadjun  40442  meadjiunlem  40445  psmeasurelem  40450  caratheodory  40505  hoidmvlelem2  40573  hoidmvlelem3  40574  hoidmvlelem4  40575  voncmpl  40598  mblvon  40616  smflimsuplem3  40791  afvres  41015  iccpartres  41118  iccelpart  41133  pfxccat1  41175  resmgmhm  41563  rhmsubclem2  41852  rhmsubcALTVlem2  41870  lincdifsn  41978  lindslinindimp2lem4  42015  lindslinindsimp2lem5  42016  lincresunit3lem2  42034  fdivmpt  42099  setrec2lem1  42205  amgmwlem  42313
  Copyright terms: Public domain W3C validator