Theorem fvres 6802

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.

Step	Hyp	Ref	Expression
1		vex 3437	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5903	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 536	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6421	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6445	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6445	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2804	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   class class class wbr 5075   ↾ cres 5592  ℩cio 6393  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-xp 5596  df-res 5602  df-iota 6395  df-fv 6445

This theorem is referenced by:  fvresd  6803  funssfv  6804  fveqres  6825  feqresmpt  6847  dffv2  6872  fvreseq0  6924  respreima  6952  fveqressseq  6966  ffvresb  7007  fnressn  7039  fressnfv  7041  fvresi  7054  funfvima  7115  funiunfv  7130  soisores  7207  isores3  7215  isoini2  7219  ofres  7561  f1oweALT  7824  offres  7835  fo1stres  7866  fo2ndres  7867  fparlem1  7961  fparlem2  7962  fsplitfpar  7968  fo2ndf  7971  f1o2ndf1  7972  fnsuppres  8016  wfrlem4OLD  8152  tfrlem1  8216  fr0g  8276  frsuc  8277  tz7.48lem  8281  seqomlem1  8290  seqomlem2  8291  seqomlem3  8292  seqomlem4  8293  onasuc  8367  onmsuc  8368  onesuc  8369  resixp  8730  fofinf1o  9103  ixpfi2  9126  ttrclss  9487  updjudhcoinlf  9699  updjudhcoinrg  9700  updjud  9701  ackbij2lem2  10005  ackbij2lem3  10006  cfsmolem  10035  alephsing  10041  fpwwe2lem7  10402  inar1  10540  addpiord  10649  mulpiord  10650  fseq1p1m1  13339  injresinj  13517  seqfeq2  13755  seqres  13759  seqf1olem2  13772  hashgval  14056  hashinf  14058  hashgval2  14102  hashf1lem1  14177  hashf1lem1OLD  14178  pfxccat1  14424  shftidt  14802  climres  15293  fsumss  15446  isumclim3  15480  fsum2dlem  15491  ackbijnn  15549  fprodss  15667  fprod2dlem  15699  iprodclim3  15719  bpolylem  15767  fprodefsum  15813  reeff1  15838  bitsf1  16162  sadcadd  16174  sadadd2  16176  eucalgcvga  16300  eucalg  16301  unbenlem  16618  strfv2d  16912  setsid  16918  setsnid  16919  setsnidOLD  16920  dfinito3  17729  dftermo3  17730  dmaf  17773  cdaf  17774  1stfcl  17923  2ndfcl  17924  resmhm  18468  resghm  18859  efgredlem  19362  gsumzaddlem  19531  dprdfadd  19632  dprdres  19640  dmdprdsplitlem  19649  dprdcntz2  19650  dmdprdsplit2lem  19657  dprdsplit  19660  dpjidcl  19670  ablfac1eu  19685  mgpf  19807  prdscrngd  19861  abvres  20108  reslmhm  20323  znf1o  20768  znunithash  20781  ltbwe  21254  subrgascl  21283  subrgasclcl  21284  smadiadetlem3  21826  lmres  22460  tx1cn  22769  tx2cn  22770  ptrescn  22799  cnmpt1st  22828  cnmpt2nd  22829  ptuncnv  22967  ptunhmeo  22968  cnextfres1  23228  prdstmdd  23284  prdsxmslem2  23694  subgnm2  23799  rescncf  24069  isncvsngp  24322  lmle  24474  ovoliunlem1  24675  ovolicc2lem4  24693  mblvol  24703  mbflimsup  24839  limcdif  25049  limcres  25059  dvres2lem  25083  dvlip  25166  dvlipcn  25167  dvlip2  25168  c1liplem1  25169  c1lip1  25170  c1lip3  25172  dvivthlem1  25181  lhop1lem  25186  lhop  25189  dvcvx  25193  ftc2ditglem  25218  itgsubstlem  25221  plyreres  25452  plyexmo  25482  aannenlem1  25497  taylthlem2  25542  ulmres  25556  ulmss  25565  pserdvlem2  25596  reeff1o  25615  reefiso  25616  reefgim  25618  recosf1o  25700  resinf1o  25701  relogcl  25740  logef  25746  logeftb  25748  logltb  25764  logcn  25811  advlog  25818  advlogexp  25819  logtayl  25824  logccv  25827  dvcxp1  25902  dvcncxp1  25905  cxpcn  25907  loglesqrt  25920  dvatan  26094  leibpi  26101  efrlim  26128  amgmlem  26148  lgamgulmlem2  26188  lgamcvg2  26213  wilthlem3  26228  ftalem3  26233  dvdsmulf1o  26352  fsumdvdsmul  26353  dchrelbas2  26394  dchrabs  26417  dchrisumlem1  26646  logdivsum  26690  log2sumbnd  26701  ostth2  26794  ostth  26796  vtxdginducedm1lem3  27917  redwlk  28049  pthdivtx  28106  pthdlem1  28143  ex-fpar  28835  sspnval  29108  hhssnv  29635  hhssmetdval  29648  foresf1o  30859  1stpreimas  31047  xpinpreima  31865  xpinpreima2  31866  cnre2csqlem  31869  rmulccn  31887  zzsnm  31918  cnzh  31929  rezh  31930  measres  32199  cntmeas  32203  cntnevol  32205  1stmbfm  32236  2ndmbfm  32237  carsggect  32294  omsmeas  32299  eulerpartgbij  32348  eulerpartlemgvv  32352  eulerpartlemgs2  32356  iwrdsplit  32363  fibp1  32377  coinfliplem  32454  coinflipprob  32455  gsumnunsn  32529  plyrecld  32537  signstres  32563  ftc2re  32587  bnj1253  33006  bnj1280  33009  f1resveqaeq  33066  subfacp1lem3  33153  subfacp1lem5  33155  erdszelem8  33169  txsconnlem  33211  cvmfolem  33250  cvmliftmolem1  33252  cvmliftlem6  33261  cvmliftlem7  33262  cvmliftlem9  33264  satfsucom  33325  satom  33327  satfvsucom  33328  satf0sucom  33344  mrsubff1  33485  msubff1  33527  fvresval  33750  dfrdg2  33780  sltres  33874  nodense  33904  nolt02o  33907  nogt01o  33908  noetainflem4  33952  funpartfv  34256  filnetlem4  34579  icoreunrn  35539  finixpnum  35771  poimirlem3  35789  poimirlem4  35790  poimirlem8  35794  poimirlem26  35812  poimirlem27  35813  itg2gt0cn  35841  areacirclem2  35875  areacirclem4  35877  eqfnun  35889  sdclem2  35909  caures  35927  ismtyres  35975  diaintclN  39079  dibintclN  39188  dihintcl  39365  fsuppssindlem1  40287  imaiinfv  40522  mzpcompact2lem  40580  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  jm2.27dlem1  40838  fnwe2lem2  40883  aomclem6  40891  deg1mhm  41039  hausgraph  41044  radcnvrat  41939  wessf1ornlem  42729  feqresmptf  42779  mccllem  43145  limcleqr  43192  limsupvaluz2  43286  supcnvlimsup  43288  limsupgtlem  43325  xlimconst2  43383  resincncf  43423  cncfperiod  43427  icccncfext  43435  cncfiooicclem1  43441  dvbdfbdioolem1  43476  dvnprodlem1  43494  dvnprodlem2  43495  itgioocnicc  43525  stoweidlem28  43576  fourierdlem18  43673  fourierdlem40  43695  fourierdlem42  43697  fourierdlem46  43700  fourierdlem51  43705  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem78  43732  fourierdlem80  43734  fourierdlem81  43735  fourierdlem82  43736  fourierdlem84  43738  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem93  43747  fourierdlem94  43748  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  sge0tsms  43925  sge0f1o  43927  sge0sup  43936  sge0less  43937  sge0ltfirp  43945  sge0resrnlem  43948  sge0resplit  43951  sge0le  43952  sge0split  43954  sge0fodjrnlem  43961  sge0iun  43964  meadjun  44007  meadjiunlem  44010  psmeasurelem  44015  caratheodory  44073  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  voncmpl  44166  mblvon  44184  smflimsuplem3  44366  afvres  44675  iccpartres  44881  iccelpart  44896  resmgmhm  45363  lincdifsn  45776  lindslinindimp2lem4  45813  lindslinindsimp2lem5  45814  lincresunit3lem2  45832  fdivmpt  45897  setrec2lem1  46410  setrecsres  46418  amgmwlem  46517