Theorem fvres 6886

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 3458	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5974	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 543	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6505	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6529	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6529	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2822	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142   class class class wbr 5100   ↾ cres 5649  ℩cio 6475  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-res 5659  df-iota 6477  df-fv 6529

This theorem is referenced by:  fvresd  6887  funssfv  6888  fveqres  6911  feqresmpt  6936  dffv2  6962  eqfnun  7018  fvreseq0  7019  respreima  7047  fveqressseq  7060  ffvresb  7107  fnressn  7141  fressnfv  7143  fvresi  7157  funfvima  7214  funiunfv  7232  soisores  7311  isores3  7319  isoini2  7323  fvresval  7342  ofres  7679  f1oweALT  7953  offres  7964  fo1stres  7996  fo2ndres  7997  fparlem1  8091  fparlem2  8092  fsplitfpar  8097  fo2ndf  8100  f1o2ndf1  8101  fnsuppres  8171  tfrlem1  8346  fr0g  8407  frsuc  8408  tz7.48lem  8412  seqomlem1  8421  seqomlem2  8422  seqomlem3  8423  seqomlem4  8424  onasuc  8497  onmsuc  8498  onesuc  8499  resixp  8915  fofinf1o  9275  ixpfi2  9293  ttrclss  9675  updjudhcoinlf  9890  updjudhcoinrg  9891  updjud  9892  ackbij2lem2  10195  ackbij2lem3  10196  cfsmolem  10227  alephsing  10233  fpwwe2lem7  10595  inar1  10733  addpiord  10842  mulpiord  10843  fseq1p1m1  13603  injresinj  13797  seqfeq2  14038  seqres  14042  seqf1olem2  14055  hashgval  14346  hashinf  14348  hashgval2  14391  hashf1lem1  14468  pfxccat1  14715  shftidt  15095  climres  15602  fsumss  15752  isumclim3  15786  fsum2dlem  15797  ackbijnn  15858  fprodss  15978  fprod2dlem  16010  iprodclim3  16030  bpolylem  16078  fprodefsum  16125  reeff1  16152  bitsf1  16480  sadcadd  16492  sadadd2  16494  eucalgcvga  16620  eucalg  16621  unbenlem  16944  strfv2d  17237  setsid  17243  setsnid  17244  dfinito3  18038  dftermo3  18039  dmaf  18082  cdaf  18083  1stfcl  18229  2ndfcl  18230  resmgmhm  18745  resmhm  18854  resghm  19272  efgredlem  19787  gsumzaddlem  19961  dprdfadd  20062  dprdres  20070  dmdprdsplitlem  20079  dprdcntz2  20080  dmdprdsplit2lem  20087  dprdsplit  20090  dpjidcl  20100  ablfac1eu  20115  rngmgpf  20203  mgpf  20294  prdscrngd  20366  abvres  20877  reslmhm  21116  znf1o  21600  znunithash  21613  ltbwe  22094  subrgascl  22116  subrgasclcl  22117  smadiadetlem3  22725  lmres  23357  tx1cn  23666  tx2cn  23667  ptrescn  23696  cnmpt1st  23725  cnmpt2nd  23726  ptuncnv  23864  ptunhmeo  23865  cnextfres1  24125  prdstmdd  24181  prdsxmslem2  24586  subgnm2  24691  rescncf  24956  isncvsngp  25208  lmle  25360  ovoliunlem1  25561  ovolicc2lem4  25579  mblvol  25589  mbflimsup  25725  limcdif  25935  limcres  25945  dvres2lem  25969  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  c1lip1  26056  c1lip3  26058  dvivthlem1  26067  lhop1lem  26072  lhop  26075  dvcvx  26079  ftc2ditglem  26104  itgsubstlem  26107  plyreres  26344  plyexmo  26374  aannenlem1  26389  taylthlem2  26434  ulmres  26448  ulmss  26457  pserdvlem2  26488  reeff1o  26507  reefiso  26508  reefgim  26510  recosf1o  26597  resinf1o  26598  relogcl  26637  logef  26643  logeftb  26645  logltb  26662  logcn  26709  advlog  26716  advlogexp  26717  logtayl  26722  logccv  26725  dvcxp1  26802  dvcncxp1  26805  cxpcn  26807  loglesqrt  26823  dvatan  26997  leibpi  27004  efrlim  27031  amgmlem  27051  lgamgulmlem2  27091  lgamcvg2  27116  wilthlem3  27131  ftalem3  27136  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  dchrelbas2  27298  dchrabs  27321  dchrisumlem1  27550  logdivsum  27594  log2sumbnd  27605  ostth2  27698  ostth  27700  ltsres  27723  nodense  27753  nolt02o  27756  nogt01o  27757  noetainflem4  27801  oniso  28361  bdayn0sf1o  28460  vtxdginducedm1lem3  29739  redwlk  29868  pthdivtx  29924  pthdlem1  29963  ex-fpar  30661  sspnval  30937  hhssnv  31464  hhssmetdval  31477  foresf1o  32700  1stpreimas  32905  cos9thpiminply  34082  xpinpreima  34200  xpinpreima2  34201  cnre2csqlem  34204  zzsnm  34253  cnzh  34262  rezh  34263  measres  34516  cntmeas  34520  cntnevol  34522  1stmbfm  34554  2ndmbfm  34555  carsggect  34612  omsmeas  34617  eulerpartgbij  34666  eulerpartlemgvv  34670  eulerpartlemgs2  34674  iwrdsplit  34681  fibp1  34695  coinfliplem  34773  coinflipprob  34774  gsumnunsn  34835  plyrecld  34840  signstres  34866  ftc2re  34889  bnj1253  35309  bnj1280  35312  f1resveqaeq  35376  noinfepregs  35426  gblacfnacd  35442  subfacp1lem3  35529  subfacp1lem5  35531  erdszelem8  35545  txsconnlem  35587  cvmfolem  35626  cvmliftmolem1  35628  cvmliftlem6  35637  cvmliftlem7  35638  cvmliftlem9  35640  satfsucom  35701  satom  35703  satfvsucom  35704  satf0sucom  35720  mrsubff1  35861  msubff1  35903  dfrdg2  36140  funpartfv  36292  filnetlem4  36738  icoreunrn  37850  finixpnum  38101  poimirlem3  38119  poimirlem4  38120  poimirlem8  38124  poimirlem26  38142  poimirlem27  38143  itg2gt0cn  38171  areacirclem2  38205  areacirclem4  38207  sdclem2  38238  caures  38256  ismtyres  38304  diaintclN  41679  dibintclN  41788  dihintcl  41965  fsuppssindlem1  43170  imaiinfv  43271  mzpcompact2lem  43329  2rexfrabdioph  43370  3rexfrabdioph  43371  4rexfrabdioph  43372  6rexfrabdioph  43373  7rexfrabdioph  43374  jm2.27dlem1  43583  fnwe2lem2  43625  aomclem6  43633  deg1mhm  43774  hausgraph  43779  radcnvrat  44887  wessf1ornlem  45760  feqresmptf  45803  mccllem  46170  limcleqr  46215  limsupvaluz2  46309  supcnvlimsup  46311  limsupgtlem  46348  xlimconst2  46406  resincncf  46446  cncfperiod  46450  icccncfext  46458  cncfiooicclem1  46464  dvbdfbdioolem1  46499  dvnprodlem1  46517  dvnprodlem2  46518  itgioocnicc  46548  stoweidlem28  46599  fourierdlem18  46696  fourierdlem40  46718  fourierdlem42  46720  fourierdlem46  46723  fourierdlem51  46728  fourierdlem70  46747  fourierdlem71  46748  fourierdlem73  46750  fourierdlem74  46751  fourierdlem75  46752  fourierdlem76  46753  fourierdlem78  46755  fourierdlem80  46757  fourierdlem81  46758  fourierdlem82  46759  fourierdlem84  46761  fourierdlem89  46766  fourierdlem90  46767  fourierdlem91  46768  fourierdlem92  46769  fourierdlem93  46770  fourierdlem94  46771  fourierdlem101  46778  fourierdlem103  46780  fourierdlem104  46781  fourierdlem111  46788  fourierdlem112  46789  fourierdlem113  46790  sge0tsms  46951  sge0f1o  46953  sge0sup  46962  sge0less  46963  sge0ltfirp  46971  sge0resrnlem  46974  sge0resplit  46977  sge0le  46978  sge0split  46980  sge0fodjrnlem  46987  sge0iun  46990  meadjun  47033  meadjiunlem  47036  psmeasurelem  47041  caratheodory  47099  hoidmvlelem2  47167  hoidmvlelem3  47168  hoidmvlelem4  47169  voncmpl  47192  mblvon  47210  smflimsuplem3  47393  cjnpoly  47480  afvres  47763  iccpartres  48021  iccelpart  48036  isubgredg  48485  isubgrgrim  48548  uhgrimisgrgric  48550  lincdifsn  49043  lindslinindimp2lem4  49080  lindslinindsimp2lem5  49081  lincresunit3lem2  49099  fdivmpt  49159  slotresfo  49517  basresposfo  49596  oppff1  49766  setrec2lem1  50311  setrecsres  50320  amgmwlem  50420