Theorem fvres 6897

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 3454	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5981	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 545	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6517	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6541	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6541	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2820	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   class class class wbr 5103   ↾ cres 5657  ℩cio 6487  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-res 5667  df-iota 6489  df-fv 6541

This theorem is used by:  fvresd  6898  funssfv  6899  fveqres  6922  feqresmpt  6947  dffv2  6973  eqfnun  7029  fvreseq0  7030  respreima  7058  fveqressseq  7072  ffvresb  7119  fnressn  7155  fressnfv  7157  fvresi  7171  funfvima  7229  funiunfv  7245  f1resveqaeq  7270  soisores  7328  isores3  7336  isoini2  7340  fvresval  7361  ofres  7697  f1oweALT  7969  offres  7980  fo1stres  8012  fo2ndres  8013  fparlem1  8109  fparlem2  8110  fsplitfpar  8115  fo2ndf  8118  f1o2ndf1  8119  fnsuppres  8189  tfrlem1  8364  fr0g  8425  frsuc  8426  tz7.48lem  8430  seqomlem1  8439  seqomlem2  8440  seqomlem3  8441  seqomlem4  8442  onasuc  8515  onmsuc  8516  onesuc  8517  resixp  8940  fofinf1o  9299  ixpfi2  9317  ttrclss  9699  updjudhcoinlf  9937  updjudhcoinrg  9938  updjud  9939  ackbij2lem2  10241  ackbij2lem3  10242  cfsmolem  10272  alephsing  10278  fpwwe2lem7  10646  inar1  10784  addpiord  10893  mulpiord  10894  fseq1p1m1  13653  injresinj  13847  seqfeq2  14089  seqres  14093  seqf1olem2  14106  hashgval  14397  hashinf  14399  hashgval2  14442  hashf1lem1  14520  pfxccat1  14771  shftidt  15155  climres  15662  fsumss  15811  isumclim3  15845  fsum2dlem  15856  ackbijnn  15917  fprodss  16035  fprod2dlem  16067  iprodclim3  16087  bpolylem  16134  fprodefsum  16181  reeff1  16208  bitsf1  16536  sadcadd  16548  sadadd2  16550  eucalgcvga  16676  eucalg  16677  unbenlem  17000  strfv2d  17293  setsid  17299  setsnid  17300  dfinito3  18094  dftermo3  18095  dmaf  18138  cdaf  18139  1stfcl  18285  2ndfcl  18286  resmgmhm  18813  resmhm  18929  resghm  19359  efgredlem  19874  gsumzaddlem  20048  dprdfadd  20149  dprdres  20157  dmdprdsplitlem  20166  dprdcntz2  20167  dmdprdsplit2lem  20174  dprdsplit  20177  dpjidcl  20187  ablfac1eu  20202  rngmgpf  20292  mgpf  20387  prdscrngd  20462  abvres  20997  reslmhm  21236  znf1o  21764  znunithash  21777  ltbwe  22260  subrgascl  22282  subrgasclcl  22283  smadiadetlem3  22890  lmres  23525  tx1cn  23835  tx2cn  23836  ptrescn  23865  cnmpt1st  23894  cnmpt2nd  23895  ptuncnv  24033  ptunhmeo  24034  cnextfres1  24294  prdstmdd  24350  prdsxmslem2  24755  subgnm2  24860  rescncf  25125  isncvsngp  25377  lmle  25529  ovoliunlem1  25730  ovolicc2lem4  25748  mblvol  25758  mbflimsup  25894  limcdif  26103  limcres  26113  dvres2lem  26137  dvlip  26220  dvlipcn  26221  dvlip2  26222  c1liplem1  26223  c1lip1  26224  c1lip3  26226  dvivthlem1  26235  lhop1lem  26240  lhop  26243  dvcvx  26247  ftc2ditglem  26272  itgsubstlem  26275  plyreres  26513  plyexmo  26545  aannenlem1  26564  taylthlem2  26610  ulmres  26624  ulmss  26633  pserdvlem2  26664  reeff1o  26683  reefiso  26684  reefgim  26686  recosf1o  26772  resinf1o  26773  relogcl  26812  logef  26818  logeftb  26820  logltb  26837  logcn  26884  advlog  26891  advlogexp  26892  logtayl  26897  logccv  26900  dvcxp1  26977  dvcncxp1  26980  cxpcn  26982  loglesqrt  26998  dvatan  27172  leibpi  27179  efrlim  27206  amgmlem  27226  lgamgulmlem2  27266  lgamcvg2  27291  wilthlem3  27306  ftalem3  27311  mpodvdsmulf1o  27430  fsumdvdsmul  27431  dvdsmulf1o  27432  dchrelbas2  27473  dchrabs  27496  dchrisumlem1  27725  logdivsum  27769  log2sumbnd  27780  ostth2  27873  ostth  27875  ltsres  27898  nodense  27928  nolt02o  27931  nogt01o  27932  noetainflem4  27976  oniso  28536  bdayn0sf1o  28635  vtxdginducedm1lem3  30001  redwlk  30130  pthdivtx  30191  pthdlem1  30231  ex-fpar  30942  sspnval  31218  hhssnv  31745  hhssmetdval  31758  foresf1o  32979  1stpreimas  33178  cos9thpiminply  34298  xpinpreima  34416  xpinpreima2  34417  cnre2csqlem  34420  zzsnm  34469  cnzh  34478  rezh  34479  measres  34733  cntmeas  34737  cntnevol  34739  1stmbfm  34771  2ndmbfm  34772  carsggect  34829  omsmeas  34834  eulerpartgbij  34883  eulerpartlemgvv  34887  eulerpartlemgs2  34891  iwrdsplit  34898  fibp1  34912  coinfliplem  34990  coinflipprob  34991  gsumnunsn  35052  plyrecld  35057  signstres  35083  ftc2re  35106  bnj1253  35526  bnj1280  35529  noinfepregs  35659  gblacfnacd  35699  subfacp1lem3  35761  subfacp1lem5  35763  erdszelem8  35777  txsconnlem  35819  cvmfolem  35858  cvmliftmolem1  35860  cvmliftlem6  35869  cvmliftlem7  35870  cvmliftlem9  35872  satfsucom  35933  satom  35935  satfvsucom  35936  satf0sucom  35952  mrsubff1  36093  msubff1  36135  dfrdg2  36372  funpartfv  36524  filnetlem4  37000  icoreunrn  38113  finixpnum  38359  poimirlem3  38372  poimirlem4  38373  poimirlem8  38377  poimirlem26  38395  poimirlem27  38396  itg2gt0cn  38424  areacirclem2  38458  areacirclem4  38460  sdclem2  38492  caures  38510  ismtyres  38558  diaintclN  41931  dibintclN  42040  dihintcl  42217  fsuppssindlem1  43437  imaiinfv  43538  mzpcompact2lem  43596  2rexfrabdioph  43637  3rexfrabdioph  43638  4rexfrabdioph  43639  6rexfrabdioph  43640  7rexfrabdioph  43641  jm2.27dlem1  43850  fnwe2lem2  43892  aomclem6  43900  deg1mhm  44041  hausgraph  44046  radcnvrat  45138  hashnna  45842  hashomiso  45848  wessf1ornlem  46017  feqresmptf  46060  mccllem  46427  limcleqr  46472  limsupvaluz2  46566  supcnvlimsup  46568  limsupgtlem  46605  xlimconst2  46663  resincncf  46703  cncfperiod  46707  icccncfext  46715  cncfiooicclem1  46721  dvbdfbdioolem1  46756  dvnprodlem1  46774  dvnprodlem2  46775  itgioocnicc  46805  stoweidlem28  46856  fourierdlem18  46953  fourierdlem40  46975  fourierdlem42  46977  fourierdlem46  46980  fourierdlem51  46985  fourierdlem70  47004  fourierdlem71  47005  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem78  47012  fourierdlem80  47014  fourierdlem81  47015  fourierdlem82  47016  fourierdlem84  47018  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem92  47026  fourierdlem93  47027  fourierdlem94  47028  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  fourierdlem113  47047  sge0tsms  47208  sge0f1o  47210  sge0sup  47219  sge0less  47220  sge0ltfirp  47228  sge0resrnlem  47231  sge0resplit  47234  sge0le  47235  sge0split  47237  sge0fodjrnlem  47244  sge0iun  47247  meadjun  47290  meadjiunlem  47293  psmeasurelem  47298  caratheodory  47356  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvlelem4  47426  voncmpl  47449  mblvon  47467  smflimsuplem3  47650  cjnpoly  47757  sqrtrrnpoly  47760  afvres  48060  iccpartres  48318  iccelpart  48333  isubgredg  48782  isubgrgrim  48845  uhgrimisgrgric  48847  lincdifsn  49354  lindslinindimp2lem4  49391  lindslinindsimp2lem5  49392  lincresunit3lem2  49410  fdivmpt  49470  slotresfo  49825  basresposfo  49904  oppff1  50074  setrec2lem1  50619  setrecsres  50628  amgmwlem  50820