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

Theorem fvres 6423
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 3394 . . . . 5 𝑥 ∈ V
21brres 5606 . . . 4 (𝐴(𝐹𝐵)𝑥 ↔ (𝐴𝐹𝑥𝐴𝐵))
32rbaib 530 . . 3 (𝐴𝐵 → (𝐴(𝐹𝐵)𝑥𝐴𝐹𝑥))
43iotabidv 6081 . 2 (𝐴𝐵 → (℩𝑥𝐴(𝐹𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5 df-fv 6105 . 2 ((𝐹𝐵)‘𝐴) = (℩𝑥𝐴(𝐹𝐵)𝑥)
6 df-fv 6105 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
74, 5, 63eqtr4g 2865 1 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156   class class class wbr 4844  cres 5313  cio 6058  cfv 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-xp 5317  df-res 5323  df-iota 6060  df-fv 6105
This theorem is referenced by:  fvresd  6424  funssfv  6425  fveqres  6446  feqresmpt  6467  dffv2  6488  fvreseq0  6535  respreima  6562  fveqressseq  6573  ffvresb  6612  fnressn  6645  fressnfv  6647  fvressn  6649  fvresi  6660  fvsnun1  6669  fvsnun2  6670  fsnunfv  6674  funfvima  6713  resfvresima  6715  funiunfv  6726  soisores  6797  isores3  6805  isoini2  6809  ovres  7026  ofres  7139  f1oweALT  7378  offres  7389  fo1stres  7420  fo2ndres  7421  curry1  7499  curry2  7502  fparlem1  7507  fparlem2  7508  fo2ndf  7514  f1o2ndf1  7515  fnsuppres  7553  wfrlem4  7649  wfrlem4OLD  7650  smores  7681  smores2  7683  tfrlem1  7704  tz7.44-2  7735  fr0g  7763  frsuc  7764  tz7.48lem  7768  seqomlem1  7777  seqomlem2  7778  seqomlem3  7779  seqomlem4  7780  onasuc  7841  onmsuc  7842  onesuc  7843  resixp  8176  fofinf1o  8476  ixpfi2  8499  ordtypelem4  8661  ordtypelem6  8663  ordtypelem7  8664  unxpwdom2  8728  cantnfres  8817  cantnfp1lem3  8820  updjudhcoinlf  9037  updjudhcoinrg  9038  updjud  9039  dfac12lem1  9246  ackbij2lem2  9343  ackbij2lem3  9344  cfsmolem  9373  alephsing  9379  ttukeylem3  9614  fpwwe2lem6  9738  fpwwe2lem8  9740  canthp1lem2  9756  inar1  9878  addpiord  9987  mulpiord  9988  addpqnq  10041  mulpqnq  10044  fseq1p1m1  12633  injresinj  12809  seqfeq2  13043  seqres  13047  seqf1olem2  13060  hashgval  13336  hashinf  13338  hashgval2  13381  hashf1lem1  13452  seqcoll  13461  swrdccat1  13677  shftidt  14041  rlimres  14508  lo1res  14509  climres  14525  isercolllem3  14616  fsumss  14675  isumclim3  14709  fsum2dlem  14720  ackbijnn  14778  fprodss  14895  fprod2dlem  14927  iprodclim3  14947  bpolylem  14995  fprodefsum  15041  reeff1  15066  bitsf1  15383  sadcaddlem  15394  sadcadd  15395  sadadd2  15397  sadaddlem  15403  sadasslem  15407  sadeq  15409  eucalgcvga  15514  eucalg  15515  unbenlem  15825  strfv2d  16112  setsid  16121  setsnid  16122  funcres  16756  dmaf  16899  cdaf  16900  1stf1  17033  2ndf1  17036  1stfcl  17038  2ndfcl  17039  prf1st  17045  prf2nd  17046  1st2ndprf  17047  uncf2  17078  diag12  17085  diag2  17086  curf2ndf  17088  yonedalem22  17119  lubval  17185  glbval  17198  resmhm  17560  resghm  17874  efgsres  18348  efgredlemd  18354  efgredlem  18357  gsumzaddlem  18518  dprdfadd  18617  dprdres  18625  dmdprdsplitlem  18634  dprdcntz2  18635  dmdprdsplit2lem  18642  dprdsplit  18645  dpjidcl  18655  ablfac1eu  18670  mgpf  18757  prdscrngd  18811  abvres  19039  reslmhm  19255  ltbwe  19677  subrgascl  19702  subrgasclcl  19703  znf1o  20103  znunithash  20116  psgndiflemB  20150  smadiadetlem3  20683  cnpresti  21303  cnprest  21304  lmres  21315  tx1cn  21623  tx2cn  21624  upxp  21637  uptx  21639  ptrescn  21653  cnmpt1st  21682  cnmpt2nd  21683  ptuncnv  21821  ptunhmeo  21822  cnextfres1  22082  prdstmdd  22137  prdsxmslem2  22544  subgnm2  22648  remetdval  22802  rescncf  22910  isncvsngp  23158  lmle  23309  lmcau  23321  ovoliunlem1  23482  ovolicc2lem4  23500  mblvol  23510  mbflimsup  23646  limcdif  23853  limcres  23863  dvreslem  23886  dvres2lem  23887  dvlip  23969  dvlipcn  23970  dvlip2  23971  c1liplem1  23972  c1lip1  23973  c1lip3  23975  dvgt0lem1  23978  dvivthlem1  23984  lhop1lem  23989  lhop  23992  dvcnvrelem1  23993  dvcvx  23996  ftc2ditglem  24021  itgsubstlem  24024  plyreres  24251  plyexmo  24281  aannenlem1  24296  taylthlem2  24341  ulmres  24355  ulmss  24364  psercn  24393  pserdvlem2  24395  reeff1o  24414  reefiso  24415  efcvx  24416  reefgim  24417  recosf1o  24495  resinf1o  24496  efif1olem4  24505  eff1olem  24508  relogcl  24535  eflog  24536  logef  24541  logeftb  24543  logltb  24559  logcn  24606  advlog  24613  advlogexp  24614  logtayl  24619  logccv  24622  dvcxp1  24694  dvcncxp1  24697  cxpcn  24699  loglesqrt  24712  asinrebnd  24841  dvatan  24875  leibpi  24882  efrlim  24909  jensen  24928  amgmlem  24929  lgamgulmlem2  24969  lgamcvg2  24994  wilthlem3  25009  ftalem3  25014  dvdsmulf1o  25133  fsumdvdsmul  25134  dchrelbas2  25175  dchrabs  25198  sum2dchr  25212  dchrisumlem1  25391  logdivsum  25435  log2sumbnd  25446  ostth2  25539  ostth  25541  vtxdginducedm1lem3  26664  wlkres  26794  redwlk  26796  pthdivtx  26852  pthdlem1  26889  sspnval  27919  hhssnv  28448  hhssmetdval  28462  foresf1o  29667  ofresid  29770  1stpreimas  29809  xpinpreima  30276  xpinpreima2  30277  cnre2csqlem  30280  rmulccn  30298  zzsnm  30329  cnzh  30338  rezh  30339  measres  30609  cntmeas  30613  cntnevol  30615  1stmbfm  30646  2ndmbfm  30647  carsggect  30704  omsmeas  30709  eulerpartgbij  30758  eulerpartlemgvv  30762  eulerpartlemgs2  30766  iwrdsplit  30773  fibp1  30787  coinfliplem  30864  coinflipprob  30865  gsumnunsn  30939  plyrecld  30950  signstres  30976  ftc2re  31000  bnj1379  31222  bnj1253  31406  bnj1280  31409  subfacp1lem3  31485  subfacp1lem5  31487  erdszelem8  31501  txsconnlem  31543  cvmfolem  31582  cvmliftmolem1  31584  cvmliftlem6  31593  cvmliftlem7  31594  cvmliftlem9  31596  mrsubff1  31732  msubff1  31774  fvresval  31985  dfrdg2  32019  sltres  32134  nodense  32161  nolt02o  32164  funpartfv  32371  filnetlem4  32695  icoreunrn  33521  finixpnum  33705  poimirlem3  33723  poimirlem4  33724  poimirlem8  33728  poimirlem26  33746  poimirlem27  33747  itg2gt0cn  33775  areacirclem2  33811  areacirclem4  33813  eqfnun  33826  sdclem2  33847  caures  33865  ismtyres  33916  diaintclN  36836  dibintclN  36945  dihintcl  37122  imaiinfv  37755  mzpcompact2lem  37813  2rexfrabdioph  37859  3rexfrabdioph  37860  4rexfrabdioph  37861  6rexfrabdioph  37862  7rexfrabdioph  37863  jm2.27dlem1  38074  fnwe2lem2  38119  fnwe2lem3  38120  aomclem6  38127  deg1mhm  38283  hausgraph  38288  radcnvrat  39010  wessf1ornlem  39857  feqresmptf  39914  mccllem  40306  limcleqr  40353  limsupvaluz2  40447  supcnvlimsup  40449  limsupgtlem  40486  xlimconst2  40538  resincncf  40565  cncfperiod  40569  icccncfext  40577  cncfiooicclem1  40583  dvbdfbdioolem1  40620  dvnprodlem1  40638  dvnprodlem2  40639  itgioocnicc  40669  stoweidlem28  40721  fourierdlem18  40818  fourierdlem40  40840  fourierdlem42  40842  fourierdlem46  40845  fourierdlem51  40850  fourierdlem70  40869  fourierdlem71  40870  fourierdlem73  40872  fourierdlem74  40873  fourierdlem75  40874  fourierdlem76  40875  fourierdlem78  40877  fourierdlem80  40879  fourierdlem81  40880  fourierdlem82  40881  fourierdlem84  40883  fourierdlem89  40888  fourierdlem90  40889  fourierdlem91  40890  fourierdlem92  40891  fourierdlem93  40892  fourierdlem94  40893  fourierdlem101  40900  fourierdlem103  40902  fourierdlem104  40903  fourierdlem111  40910  fourierdlem112  40911  fourierdlem113  40912  sge0tsms  41073  sge0f1o  41075  sge0sup  41084  sge0less  41085  sge0ltfirp  41093  sge0resrnlem  41096  sge0resplit  41099  sge0le  41100  sge0split  41102  sge0fodjrnlem  41109  sge0iun  41112  meadjun  41155  meadjiunlem  41158  psmeasurelem  41163  caratheodory  41221  hoidmvlelem2  41289  hoidmvlelem3  41290  hoidmvlelem4  41291  voncmpl  41314  mblvon  41332  smflimsuplem3  41507  afvres  41758  iccpartres  41926  iccelpart  41941  pfxccat1  41982  resmgmhm  42363  rhmsubclem2  42652  rhmsubcALTVlem2  42670  lincdifsn  42778  lindslinindimp2lem4  42815  lindslinindsimp2lem5  42816  lincresunit3lem2  42834  fdivmpt  42899  setrec2lem1  43005  setrecsres  43013  amgmwlem  43116
  Copyright terms: Public domain W3C validator