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

Theorem fvres 6245
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 3234 . . . . 5 𝑥 ∈ V
21brres 5437 . . . 4 (𝐴(𝐹𝐵)𝑥 ↔ (𝐴𝐹𝑥𝐴𝐵))
32rbaib 967 . . 3 (𝐴𝐵 → (𝐴(𝐹𝐵)𝑥𝐴𝐹𝑥))
43iotabidv 5910 . 2 (𝐴𝐵 → (℩𝑥𝐴(𝐹𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5 df-fv 5934 . 2 ((𝐹𝐵)‘𝐴) = (℩𝑥𝐴(𝐹𝐵)𝑥)
6 df-fv 5934 . 2 (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
74, 5, 63eqtr4g 2710 1 (𝐴𝐵 → ((𝐹𝐵)‘𝐴) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030   class class class wbr 4685  cres 5145  cio 5887  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-xp 5149  df-res 5155  df-iota 5889  df-fv 5934
This theorem is referenced by:  fvresd  6246  funssfv  6247  fveqres  6268  feqresmpt  6289  dffv2  6310  fvreseq0  6357  respreima  6384  fveqressseq  6395  ffvresb  6434  fnressn  6465  fressnfv  6467  fvressn  6469  fvresi  6480  fvsnun1  6489  fvsnun2  6490  fsnunfv  6494  funfvima  6532  resfvresima  6534  funiunfv  6546  soisores  6617  isores3  6625  isoini2  6629  ovres  6842  ofres  6955  f1oweALT  7194  offres  7205  fo1stres  7236  fo2ndres  7237  curry1  7314  curry2  7317  fparlem1  7322  fparlem2  7323  fo2ndf  7329  f1o2ndf1  7330  fnsuppres  7367  wfrlem4  7463  smores  7494  smores2  7496  tfrlem1  7517  tz7.44-2  7548  fr0g  7576  frsuc  7577  tz7.48lem  7581  seqomlem1  7590  seqomlem2  7591  seqomlem3  7592  seqomlem4  7593  onasuc  7653  onmsuc  7654  onesuc  7655  resixp  7985  fofinf1o  8282  ixpfi2  8305  ordtypelem4  8467  ordtypelem6  8469  ordtypelem7  8470  unxpwdom2  8534  cantnfres  8612  cantnfp1lem3  8615  dfac12lem1  9003  ackbij2lem2  9100  ackbij2lem3  9101  cfsmolem  9130  alephsing  9136  ttukeylem3  9371  fpwwe2lem6  9495  fpwwe2lem8  9497  fpwwe2lem9  9498  canthp1lem2  9513  inar1  9635  addpiord  9744  mulpiord  9745  addpqnq  9798  mulpqnq  9801  fseq1p1m1  12452  injresinj  12629  seqfeq2  12864  seqres  12868  seqf1olem2  12881  hashgval  13160  hashinf  13162  hashgval2  13205  hashf1lem1  13277  seqcoll  13286  swrdccat1  13503  shftidt  13866  rlimres  14333  lo1res  14334  climres  14350  isercolllem3  14441  fsumss  14500  isumclim3  14534  fsum2dlem  14545  ackbijnn  14604  fprodss  14722  fprod2dlem  14754  iprodclim3  14775  bpolylem  14823  fprodefsum  14869  reeff1  14894  bitsf1  15215  sadcaddlem  15226  sadcadd  15227  sadadd2  15229  sadaddlem  15235  sadasslem  15239  sadeq  15241  eucalgcvga  15346  eucalg  15347  unbenlem  15659  strfv2d  15952  setsid  15961  setsnid  15962  funcres  16603  dmaf  16746  cdaf  16747  1stf1  16879  2ndf1  16882  1stfcl  16884  2ndfcl  16885  prf1st  16891  prf2nd  16892  1st2ndprf  16893  uncf2  16924  diag12  16931  diag2  16932  curf2ndf  16934  yonedalem22  16965  lubval  17031  glbval  17044  resmhm  17406  resghm  17723  efgsres  18197  efgredlemd  18203  efgredlem  18206  gsumzaddlem  18367  dprdfadd  18465  dprdres  18473  dmdprdsplitlem  18482  dprdcntz2  18483  dmdprdsplit2lem  18490  dprdsplit  18493  dpjidcl  18503  ablfac1eu  18518  mgpf  18605  prdscrngd  18659  abvres  18887  reslmhm  19100  ltbwe  19520  subrgascl  19546  subrgasclcl  19547  znf1o  19948  znunithash  19961  psgndiflemB  19994  smadiadetlem3  20522  cnpresti  21140  cnprest  21141  lmres  21152  tx1cn  21460  tx2cn  21461  upxp  21474  uptx  21476  ptrescn  21490  cnmpt1st  21519  cnmpt2nd  21520  ptuncnv  21658  ptunhmeo  21659  cnextfres1  21919  prdstmdd  21974  prdsxmslem2  22381  subgnm2  22485  remetdval  22639  rescncf  22747  isncvsngp  22995  lmle  23145  lmcau  23157  ovoliunlem1  23316  ovolicc2lem4  23334  mblvol  23344  mbflimsup  23478  limcdif  23685  limcres  23695  dvreslem  23718  dvres2lem  23719  dvlip  23801  dvlipcn  23802  dvlip2  23803  c1liplem1  23804  c1lip1  23805  c1lip3  23807  dvgt0lem1  23810  dvivthlem1  23816  lhop1lem  23821  lhop  23824  dvcnvrelem1  23825  dvcvx  23828  ftc2ditglem  23853  itgsubstlem  23856  plyreres  24083  plyexmo  24113  aannenlem1  24128  taylthlem2  24173  ulmres  24187  ulmss  24196  psercn  24225  pserdvlem2  24227  reeff1o  24246  reefiso  24247  efcvx  24248  reefgim  24249  recosf1o  24326  resinf1o  24327  efif1olem4  24336  eff1olem  24339  relogcl  24367  eflog  24368  logef  24373  logeftb  24375  logltb  24391  logcn  24438  advlog  24445  advlogexp  24446  logtayl  24451  logccv  24454  dvcxp1  24526  dvcncxp1  24529  cxpcn  24531  loglesqrt  24544  asinrebnd  24673  dvatan  24707  leibpi  24714  efrlim  24741  jensen  24760  amgmlem  24761  lgamgulmlem2  24801  lgamcvg2  24826  wilthlem3  24841  ftalem3  24846  dvdsmulf1o  24965  fsumdvdsmul  24966  dchrelbas2  25007  dchrabs  25030  sum2dchr  25044  dchrisumlem1  25223  logdivsum  25267  log2sumbnd  25278  ostth2  25371  ostth  25373  vtxdginducedm1lem3  26493  wlkres  26623  redwlk  26625  pthdivtx  26681  pthdlem1  26718  sspnval  27720  hhssnv  28249  hhssmetdval  28263  foresf1o  29469  ofresid  29572  1stpreimas  29611  xpinpreima  30080  xpinpreima2  30081  cnre2csqlem  30084  rmulccn  30102  zzsnm  30133  cnzh  30142  rezh  30143  measres  30413  cntmeas  30417  cntnevol  30419  1stmbfm  30450  2ndmbfm  30451  carsggect  30508  omsmeas  30513  eulerpartgbij  30562  eulerpartlemgvv  30566  eulerpartlemgs2  30570  iwrdsplit  30577  fibp1  30591  coinfliplem  30668  coinflipprob  30669  gsumnunsn  30743  plyrecld  30754  signstres  30780  ftc2re  30804  bnj1379  31027  bnj1253  31211  bnj1280  31214  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem8  31306  txsconnlem  31348  cvmfolem  31387  cvmliftmolem1  31389  cvmliftlem6  31398  cvmliftlem7  31399  cvmliftlem9  31401  mrsubff1  31537  msubff1  31579  fvresval  31791  dfrdg2  31825  sltres  31940  nodense  31967  nolt02o  31970  funpartfv  32177  filnetlem4  32501  icoreunrn  33337  finixpnum  33524  poimirlem3  33542  poimirlem4  33543  poimirlem8  33547  poimirlem26  33565  poimirlem27  33566  itg2gt0cn  33595  areacirclem2  33631  areacirclem4  33633  eqfnun  33646  sdclem2  33668  caures  33686  ismtyres  33737  diaintclN  36664  dibintclN  36773  dihintcl  36950  imaiinfv  37573  mzpcompact2lem  37631  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  jm2.27dlem1  37893  fnwe2lem2  37938  fnwe2lem3  37939  aomclem6  37946  deg1mhm  38102  hausgraph  38107  radcnvrat  38830  wessf1ornlem  39685  feqresmptf  39747  mccllem  40147  limcperiod  40178  limcleqr  40194  limclner  40201  limsupvaluz2  40288  supcnvlimsup  40290  limsupgtlem  40327  xlimconst2  40379  resincncf  40406  cncfperiod  40410  icccncfext  40418  cncfiooicclem1  40424  dvbdfbdioolem1  40461  dvnprodlem1  40479  dvnprodlem2  40480  itgioocnicc  40511  stoweidlem28  40563  fourierdlem18  40660  fourierdlem40  40682  fourierdlem42  40684  fourierdlem46  40687  fourierdlem51  40692  fourierdlem70  40711  fourierdlem71  40712  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem80  40721  fourierdlem81  40722  fourierdlem82  40723  fourierdlem84  40725  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem93  40734  fourierdlem94  40735  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  sge0tsms  40915  sge0f1o  40917  sge0sup  40926  sge0less  40927  sge0ltfirp  40935  sge0resrnlem  40938  sge0resplit  40941  sge0le  40942  sge0split  40944  sge0fodjrnlem  40951  sge0iun  40954  meadjun  40997  meadjiunlem  41000  psmeasurelem  41005  caratheodory  41063  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  voncmpl  41156  mblvon  41174  smflimsuplem3  41349  afvres  41573  iccpartres  41679  iccelpart  41694  pfxccat1  41735  resmgmhm  42123  rhmsubclem2  42412  rhmsubcALTVlem2  42430  lincdifsn  42538  lindslinindimp2lem4  42575  lindslinindsimp2lem5  42576  lincresunit3lem2  42594  fdivmpt  42659  setrec2lem1  42765  setrecsres  42773  amgmwlem  42876
  Copyright terms: Public domain W3C validator