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

Theorem fvres 6348
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 3354 . . . . 5 𝑥 ∈ V
21brres 5543 . . . 4 (𝐴(𝐹𝐵)𝑥 ↔ (𝐴𝐹𝑥𝐴𝐵))
32rbaib 528 . . 3 (𝐴𝐵 → (𝐴(𝐹𝐵)𝑥𝐴𝐹𝑥))
43iotabidv 6015 . 2 (𝐴𝐵 → (℩𝑥𝐴(𝐹𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5 df-fv 6039 . 2 ((𝐹𝐵)‘𝐴) = (℩𝑥𝐴(𝐹𝐵)𝑥)
6 df-fv 6039 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
74, 5, 63eqtr4g 2830 1 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145   class class class wbr 4786  cres 5251  cio 5992  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-res 5261  df-iota 5994  df-fv 6039
This theorem is referenced by:  fvresd  6349  funssfv  6350  fveqres  6371  feqresmpt  6392  dffv2  6413  fvreseq0  6460  respreima  6487  fveqressseq  6498  ffvresb  6536  fnressn  6568  fressnfv  6570  fvressn  6572  fvresi  6583  fvsnun1  6592  fvsnun2  6593  fsnunfv  6597  funfvima  6635  resfvresima  6637  funiunfv  6649  soisores  6720  isores3  6728  isoini2  6732  ovres  6947  ofres  7060  f1oweALT  7299  offres  7310  fo1stres  7341  fo2ndres  7342  curry1  7420  curry2  7423  fparlem1  7428  fparlem2  7429  fo2ndf  7435  f1o2ndf1  7436  fnsuppres  7474  wfrlem4  7570  wfrlem4OLD  7571  smores  7602  smores2  7604  tfrlem1  7625  tz7.44-2  7656  fr0g  7684  frsuc  7685  tz7.48lem  7689  seqomlem1  7698  seqomlem2  7699  seqomlem3  7700  seqomlem4  7701  onasuc  7762  onmsuc  7763  onesuc  7764  resixp  8097  fofinf1o  8397  ixpfi2  8420  ordtypelem4  8582  ordtypelem6  8584  ordtypelem7  8585  unxpwdom2  8649  cantnfres  8738  cantnfp1lem3  8741  updjudhcoinlf  8958  updjudhcoinrg  8959  updjud  8960  dfac12lem1  9167  ackbij2lem2  9264  ackbij2lem3  9265  cfsmolem  9294  alephsing  9300  ttukeylem3  9535  fpwwe2lem6  9659  fpwwe2lem8  9661  fpwwe2lem9  9662  canthp1lem2  9677  inar1  9799  addpiord  9908  mulpiord  9909  addpqnq  9962  mulpqnq  9965  fseq1p1m1  12621  injresinj  12797  seqfeq2  13031  seqres  13035  seqf1olem2  13048  hashgval  13324  hashinf  13326  hashgval2  13369  hashf1lem1  13441  seqcoll  13450  swrdccat1  13666  shftidt  14030  rlimres  14497  lo1res  14498  climres  14514  isercolllem3  14605  fsumss  14664  isumclim3  14698  fsum2dlem  14709  ackbijnn  14767  fprodss  14885  fprod2dlem  14917  iprodclim3  14937  bpolylem  14985  fprodefsum  15031  reeff1  15056  bitsf1  15376  sadcaddlem  15387  sadcadd  15388  sadadd2  15390  sadaddlem  15396  sadasslem  15400  sadeq  15402  eucalgcvga  15507  eucalg  15508  unbenlem  15819  strfv2d  16112  setsid  16121  setsnid  16122  funcres  16763  dmaf  16906  cdaf  16907  1stf1  17040  2ndf1  17043  1stfcl  17045  2ndfcl  17046  prf1st  17052  prf2nd  17053  1st2ndprf  17054  uncf2  17085  diag12  17092  diag2  17093  curf2ndf  17095  yonedalem22  17126  lubval  17192  glbval  17205  resmhm  17567  resghm  17884  efgsres  18358  efgredlemd  18364  efgredlem  18367  gsumzaddlem  18528  dprdfadd  18627  dprdres  18635  dmdprdsplitlem  18644  dprdcntz2  18645  dmdprdsplit2lem  18652  dprdsplit  18655  dpjidcl  18665  ablfac1eu  18680  mgpf  18767  prdscrngd  18821  abvres  19049  reslmhm  19265  ltbwe  19687  subrgascl  19713  subrgasclcl  19714  znf1o  20115  znunithash  20128  psgndiflemB  20162  smadiadetlem3  20693  cnpresti  21313  cnprest  21314  lmres  21325  tx1cn  21633  tx2cn  21634  upxp  21647  uptx  21649  ptrescn  21663  cnmpt1st  21692  cnmpt2nd  21693  ptuncnv  21831  ptunhmeo  21832  cnextfres1  22092  prdstmdd  22147  prdsxmslem2  22554  subgnm2  22658  remetdval  22812  rescncf  22920  isncvsngp  23168  lmle  23318  lmcau  23330  ovoliunlem1  23490  ovolicc2lem4  23508  mblvol  23518  mbflimsup  23653  limcdif  23860  limcres  23870  dvreslem  23893  dvres2lem  23894  dvlip  23976  dvlipcn  23977  dvlip2  23978  c1liplem1  23979  c1lip1  23980  c1lip3  23982  dvgt0lem1  23985  dvivthlem1  23991  lhop1lem  23996  lhop  23999  dvcnvrelem1  24000  dvcvx  24003  ftc2ditglem  24028  itgsubstlem  24031  plyreres  24258  plyexmo  24288  aannenlem1  24303  taylthlem2  24348  ulmres  24362  ulmss  24371  psercn  24400  pserdvlem2  24402  reeff1o  24421  reefiso  24422  efcvx  24423  reefgim  24424  recosf1o  24502  resinf1o  24503  efif1olem4  24512  eff1olem  24515  relogcl  24543  eflog  24544  logef  24549  logeftb  24551  logltb  24567  logcn  24614  advlog  24621  advlogexp  24622  logtayl  24627  logccv  24630  dvcxp1  24702  dvcncxp1  24705  cxpcn  24707  loglesqrt  24720  asinrebnd  24849  dvatan  24883  leibpi  24890  efrlim  24917  jensen  24936  amgmlem  24937  lgamgulmlem2  24977  lgamcvg2  25002  wilthlem3  25017  ftalem3  25022  dvdsmulf1o  25141  fsumdvdsmul  25142  dchrelbas2  25183  dchrabs  25206  sum2dchr  25220  dchrisumlem1  25399  logdivsum  25443  log2sumbnd  25454  ostth2  25547  ostth  25549  vtxdginducedm1lem3  26672  wlkres  26802  redwlk  26804  pthdivtx  26860  pthdlem1  26897  sspnval  27932  hhssnv  28461  hhssmetdval  28475  foresf1o  29681  ofresid  29784  1stpreimas  29823  xpinpreima  30292  xpinpreima2  30293  cnre2csqlem  30296  rmulccn  30314  zzsnm  30345  cnzh  30354  rezh  30355  measres  30625  cntmeas  30629  cntnevol  30631  1stmbfm  30662  2ndmbfm  30663  carsggect  30720  omsmeas  30725  eulerpartgbij  30774  eulerpartlemgvv  30778  eulerpartlemgs2  30782  iwrdsplit  30789  fibp1  30803  coinfliplem  30880  coinflipprob  30881  gsumnunsn  30955  plyrecld  30966  signstres  30992  ftc2re  31016  bnj1379  31239  bnj1253  31423  bnj1280  31426  subfacp1lem3  31502  subfacp1lem5  31504  erdszelem8  31518  txsconnlem  31560  cvmfolem  31599  cvmliftmolem1  31601  cvmliftlem6  31610  cvmliftlem7  31611  cvmliftlem9  31613  mrsubff1  31749  msubff1  31791  fvresval  32003  dfrdg2  32037  sltres  32152  nodense  32179  nolt02o  32182  funpartfv  32389  filnetlem4  32713  icoreunrn  33544  finixpnum  33727  poimirlem3  33745  poimirlem4  33746  poimirlem8  33750  poimirlem26  33768  poimirlem27  33769  itg2gt0cn  33797  areacirclem2  33833  areacirclem4  33835  eqfnun  33848  sdclem2  33870  caures  33888  ismtyres  33939  diaintclN  36868  dibintclN  36977  dihintcl  37154  imaiinfv  37782  mzpcompact2lem  37840  2rexfrabdioph  37886  3rexfrabdioph  37887  4rexfrabdioph  37888  6rexfrabdioph  37889  7rexfrabdioph  37890  jm2.27dlem1  38102  fnwe2lem2  38147  fnwe2lem3  38148  aomclem6  38155  deg1mhm  38311  hausgraph  38316  radcnvrat  39039  wessf1ornlem  39891  feqresmptf  39951  mccllem  40347  limcperiod  40378  limcleqr  40394  limclner  40401  limsupvaluz2  40488  supcnvlimsup  40490  limsupgtlem  40527  xlimconst2  40579  resincncf  40606  cncfperiod  40610  icccncfext  40618  cncfiooicclem1  40624  dvbdfbdioolem1  40661  dvnprodlem1  40679  dvnprodlem2  40680  itgioocnicc  40710  stoweidlem28  40762  fourierdlem18  40859  fourierdlem40  40881  fourierdlem42  40883  fourierdlem46  40886  fourierdlem51  40891  fourierdlem70  40910  fourierdlem71  40911  fourierdlem73  40913  fourierdlem74  40914  fourierdlem75  40915  fourierdlem76  40916  fourierdlem78  40918  fourierdlem80  40920  fourierdlem81  40921  fourierdlem82  40922  fourierdlem84  40924  fourierdlem89  40929  fourierdlem90  40930  fourierdlem91  40931  fourierdlem92  40932  fourierdlem93  40933  fourierdlem94  40934  fourierdlem101  40941  fourierdlem103  40943  fourierdlem104  40944  fourierdlem111  40951  fourierdlem112  40952  fourierdlem113  40953  sge0tsms  41114  sge0f1o  41116  sge0sup  41125  sge0less  41126  sge0ltfirp  41134  sge0resrnlem  41137  sge0resplit  41140  sge0le  41141  sge0split  41143  sge0fodjrnlem  41150  sge0iun  41153  meadjun  41196  meadjiunlem  41199  psmeasurelem  41204  caratheodory  41262  hoidmvlelem2  41330  hoidmvlelem3  41331  hoidmvlelem4  41332  voncmpl  41355  mblvon  41373  smflimsuplem3  41548  afvres  41772  iccpartres  41882  iccelpart  41897  pfxccat1  41938  resmgmhm  42326  rhmsubclem2  42615  rhmsubcALTVlem2  42633  lincdifsn  42741  lindslinindimp2lem4  42778  lindslinindsimp2lem5  42779  lincresunit3lem2  42797  fdivmpt  42862  setrec2lem1  42968  setrecsres  42976  amgmwlem  43079
  Copyright terms: Public domain W3C validator