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

Theorem fvres 6668
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 3447 . . . . 5 𝑥 ∈ V
21brresi 5831 . . . 4 (𝐴(𝐹𝐵)𝑥 ↔ (𝐴𝐵𝐴𝐹𝑥))
32baib 539 . . 3 (𝐴𝐵 → (𝐴(𝐹𝐵)𝑥𝐴𝐹𝑥))
43iotabidv 6312 . 2 (𝐴𝐵 → (℩𝑥𝐴(𝐹𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5 df-fv 6336 . 2 ((𝐹𝐵)‘𝐴) = (℩𝑥𝐴(𝐹𝐵)𝑥)
6 df-fv 6336 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
74, 5, 63eqtr4g 2861 1 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112   class class class wbr 5033  cres 5525  cio 6285  cfv 6328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-xp 5529  df-res 5535  df-iota 6287  df-fv 6336
This theorem is referenced by:  fvresd  6669  funssfv  6670  fveqres  6691  feqresmpt  6713  dffv2  6737  fvreseq0  6789  respreima  6817  fveqressseq  6828  ffvresb  6869  fnressn  6901  fressnfv  6903  fvresi  6916  funfvima  6974  funiunfv  6989  soisores  7063  isores3  7071  isoini2  7075  ofres  7409  f1oweALT  7659  offres  7670  fo1stres  7701  fo2ndres  7702  fparlem1  7794  fparlem2  7795  fsplitfpar  7801  fo2ndf  7804  f1o2ndf1  7805  fnsuppres  7844  wfrlem4  7945  tfrlem1  7999  fr0g  8058  frsuc  8059  tz7.48lem  8064  seqomlem1  8073  seqomlem2  8074  seqomlem3  8075  seqomlem4  8076  onasuc  8140  onmsuc  8141  onesuc  8142  resixp  8484  fofinf1o  8787  ixpfi2  8810  updjudhcoinlf  9349  updjudhcoinrg  9350  updjud  9351  ackbij2lem2  9655  ackbij2lem3  9656  cfsmolem  9685  alephsing  9691  fpwwe2lem8  10052  inar1  10190  addpiord  10299  mulpiord  10300  fseq1p1m1  12980  injresinj  13157  seqfeq2  13393  seqres  13397  seqf1olem2  13410  hashgval  13693  hashinf  13695  hashgval2  13739  hashf1lem1  13813  pfxccat1  14059  shftidt  14437  climres  14928  fsumss  15078  isumclim3  15110  fsum2dlem  15121  ackbijnn  15179  fprodss  15298  fprod2dlem  15330  iprodclim3  15350  bpolylem  15398  fprodefsum  15444  reeff1  15469  bitsf1  15789  sadcadd  15801  sadadd2  15803  eucalgcvga  15924  eucalg  15925  unbenlem  16238  strfv2d  16525  setsid  16534  setsnid  16535  dmaf  17305  cdaf  17306  1stfcl  17443  2ndfcl  17444  resmhm  17981  resghm  18370  efgredlem  18869  gsumzaddlem  19038  dprdfadd  19139  dprdres  19147  dmdprdsplitlem  19156  dprdcntz2  19157  dmdprdsplit2lem  19164  dprdsplit  19167  dpjidcl  19177  ablfac1eu  19192  mgpf  19309  prdscrngd  19363  abvres  19607  reslmhm  19821  znf1o  20247  znunithash  20260  ltbwe  20716  subrgascl  20741  subrgasclcl  20742  smadiadetlem3  21277  lmres  21909  tx1cn  22218  tx2cn  22219  ptrescn  22248  cnmpt1st  22277  cnmpt2nd  22278  ptuncnv  22416  ptunhmeo  22417  cnextfres1  22677  prdstmdd  22733  prdsxmslem2  23140  subgnm2  23244  rescncf  23506  isncvsngp  23758  lmle  23909  ovoliunlem1  24110  ovolicc2lem4  24128  mblvol  24138  mbflimsup  24274  limcdif  24483  limcres  24493  dvres2lem  24517  dvlip  24600  dvlipcn  24601  dvlip2  24602  c1liplem1  24603  c1lip1  24604  c1lip3  24606  dvivthlem1  24615  lhop1lem  24620  lhop  24623  dvcvx  24627  ftc2ditglem  24652  itgsubstlem  24655  plyreres  24883  plyexmo  24913  aannenlem1  24928  taylthlem2  24973  ulmres  24987  ulmss  24996  pserdvlem2  25027  reeff1o  25046  reefiso  25047  reefgim  25049  recosf1o  25131  resinf1o  25132  relogcl  25171  logef  25177  logeftb  25179  logltb  25195  logcn  25242  advlog  25249  advlogexp  25250  logtayl  25255  logccv  25258  dvcxp1  25333  dvcncxp1  25336  cxpcn  25338  loglesqrt  25351  dvatan  25525  leibpi  25532  efrlim  25559  amgmlem  25579  lgamgulmlem2  25619  lgamcvg2  25644  wilthlem3  25659  ftalem3  25664  dvdsmulf1o  25783  fsumdvdsmul  25784  dchrelbas2  25825  dchrabs  25848  dchrisumlem1  26077  logdivsum  26121  log2sumbnd  26132  ostth2  26225  ostth  26227  vtxdginducedm1lem3  27335  redwlk  27466  pthdivtx  27522  pthdlem1  27559  ex-fpar  28251  sspnval  28524  hhssnv  29051  hhssmetdval  29064  foresf1o  30277  1stpreimas  30469  xpinpreima  31263  xpinpreima2  31264  cnre2csqlem  31267  rmulccn  31285  zzsnm  31316  cnzh  31325  rezh  31326  measres  31595  cntmeas  31599  cntnevol  31601  1stmbfm  31632  2ndmbfm  31633  carsggect  31690  omsmeas  31695  eulerpartgbij  31744  eulerpartlemgvv  31748  eulerpartlemgs2  31752  iwrdsplit  31759  fibp1  31773  coinfliplem  31850  coinflipprob  31851  gsumnunsn  31925  plyrecld  31933  signstres  31959  ftc2re  31983  bnj1253  32403  bnj1280  32406  f1resveqaeq  32472  subfacp1lem3  32543  subfacp1lem5  32545  erdszelem8  32559  txsconnlem  32601  cvmfolem  32640  cvmliftmolem1  32642  cvmliftlem6  32651  cvmliftlem7  32652  cvmliftlem9  32654  satfsucom  32715  satom  32717  satfvsucom  32718  satf0sucom  32734  mrsubff1  32875  msubff1  32917  fvresval  33124  dfrdg2  33154  sltres  33283  nodense  33310  nolt02o  33313  funpartfv  33520  filnetlem4  33843  icoreunrn  34777  finixpnum  35041  poimirlem3  35059  poimirlem4  35060  poimirlem8  35064  poimirlem26  35082  poimirlem27  35083  itg2gt0cn  35111  areacirclem2  35145  areacirclem4  35147  eqfnun  35159  sdclem2  35179  caures  35197  ismtyres  35245  diaintclN  38353  dibintclN  38462  dihintcl  38639  fsuppssindlem1  39454  imaiinfv  39631  mzpcompact2lem  39689  2rexfrabdioph  39734  3rexfrabdioph  39735  4rexfrabdioph  39736  6rexfrabdioph  39737  7rexfrabdioph  39738  jm2.27dlem1  39947  fnwe2lem2  39992  aomclem6  40000  deg1mhm  40148  hausgraph  40153  radcnvrat  41015  wessf1ornlem  41808  feqresmptf  41862  mccllem  42236  limcleqr  42283  limsupvaluz2  42377  supcnvlimsup  42379  limsupgtlem  42416  xlimconst2  42474  resincncf  42514  cncfperiod  42518  icccncfext  42526  cncfiooicclem1  42532  dvbdfbdioolem1  42567  dvnprodlem1  42585  dvnprodlem2  42586  itgioocnicc  42616  stoweidlem28  42667  fourierdlem18  42764  fourierdlem40  42786  fourierdlem42  42788  fourierdlem46  42791  fourierdlem51  42796  fourierdlem70  42815  fourierdlem71  42816  fourierdlem73  42818  fourierdlem74  42819  fourierdlem75  42820  fourierdlem76  42821  fourierdlem78  42823  fourierdlem80  42825  fourierdlem81  42826  fourierdlem82  42827  fourierdlem84  42829  fourierdlem89  42834  fourierdlem90  42835  fourierdlem91  42836  fourierdlem92  42837  fourierdlem93  42838  fourierdlem94  42839  fourierdlem101  42846  fourierdlem103  42848  fourierdlem104  42849  fourierdlem111  42856  fourierdlem112  42857  fourierdlem113  42858  sge0tsms  43016  sge0f1o  43018  sge0sup  43027  sge0less  43028  sge0ltfirp  43036  sge0resrnlem  43039  sge0resplit  43042  sge0le  43043  sge0split  43045  sge0fodjrnlem  43052  sge0iun  43055  meadjun  43098  meadjiunlem  43101  psmeasurelem  43106  caratheodory  43164  hoidmvlelem2  43232  hoidmvlelem3  43233  hoidmvlelem4  43234  voncmpl  43257  mblvon  43275  smflimsuplem3  43450  afvres  43725  iccpartres  43932  iccelpart  43947  resmgmhm  44415  lincdifsn  44830  lindslinindimp2lem4  44867  lindslinindsimp2lem5  44868  lincresunit3lem2  44886  fdivmpt  44951  setrec2lem1  45220  setrecsres  45228  amgmwlem  45327
  Copyright terms: Public domain W3C validator