Theorem fvres 6853

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 3444	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5947	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6476	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6500	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6500	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2796	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   class class class wbr 5098   ↾ cres 5626  ℩cio 6446  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-res 5636  df-iota 6448  df-fv 6500

This theorem is referenced by:  fvresd  6854  funssfv  6855  fveqres  6878  feqresmpt  6903  dffv2  6929  eqfnun  6982  fvreseq0  6983  respreima  7011  fveqressseq  7024  ffvresb  7070  fnressn  7103  fressnfv  7105  fvresi  7119  funfvima  7176  funiunfv  7194  soisores  7273  isores3  7281  isoini2  7285  fvresval  7304  ofres  7641  f1oweALT  7916  offres  7927  fo1stres  7959  fo2ndres  7960  fparlem1  8054  fparlem2  8055  fsplitfpar  8060  fo2ndf  8063  f1o2ndf1  8064  fnsuppres  8133  tfrlem1  8307  fr0g  8367  frsuc  8368  tz7.48lem  8372  seqomlem1  8381  seqomlem2  8382  seqomlem3  8383  seqomlem4  8384  onasuc  8455  onmsuc  8456  onesuc  8457  resixp  8871  fofinf1o  9232  ixpfi2  9250  ttrclss  9629  updjudhcoinlf  9844  updjudhcoinrg  9845  updjud  9846  ackbij2lem2  10149  ackbij2lem3  10150  cfsmolem  10180  alephsing  10186  fpwwe2lem7  10548  inar1  10686  addpiord  10795  mulpiord  10796  fseq1p1m1  13514  injresinj  13707  seqfeq2  13948  seqres  13952  seqf1olem2  13965  hashgval  14256  hashinf  14258  hashgval2  14301  hashf1lem1  14378  pfxccat1  14625  shftidt  15005  climres  15498  fsumss  15648  isumclim3  15682  fsum2dlem  15693  ackbijnn  15751  fprodss  15871  fprod2dlem  15903  iprodclim3  15923  bpolylem  15971  fprodefsum  16018  reeff1  16045  bitsf1  16373  sadcadd  16385  sadadd2  16387  eucalgcvga  16513  eucalg  16514  unbenlem  16836  strfv2d  17128  setsid  17134  setsnid  17135  dfinito3  17929  dftermo3  17930  dmaf  17973  cdaf  17974  1stfcl  18120  2ndfcl  18121  resmgmhm  18636  resmhm  18745  resghm  19161  efgredlem  19676  gsumzaddlem  19850  dprdfadd  19951  dprdres  19959  dmdprdsplitlem  19968  dprdcntz2  19969  dmdprdsplit2lem  19976  dprdsplit  19979  dpjidcl  19989  ablfac1eu  20004  rngmgpf  20092  mgpf  20183  prdscrngd  20257  abvres  20764  reslmhm  21004  znf1o  21506  znunithash  21519  ltbwe  21999  subrgascl  22021  subrgasclcl  22022  smadiadetlem3  22612  lmres  23244  tx1cn  23553  tx2cn  23554  ptrescn  23583  cnmpt1st  23612  cnmpt2nd  23613  ptuncnv  23751  ptunhmeo  23752  cnextfres1  24012  prdstmdd  24068  prdsxmslem2  24473  subgnm2  24578  rescncf  24846  isncvsngp  25105  lmle  25257  ovoliunlem1  25459  ovolicc2lem4  25477  mblvol  25487  mbflimsup  25623  limcdif  25833  limcres  25843  dvres2lem  25867  dvlip  25954  dvlipcn  25955  dvlip2  25956  c1liplem1  25957  c1lip1  25958  c1lip3  25960  dvivthlem1  25969  lhop1lem  25974  lhop  25977  dvcvx  25981  ftc2ditglem  26008  itgsubstlem  26011  plyreres  26246  plyexmo  26277  aannenlem1  26292  taylthlem2  26338  taylthlem2OLD  26339  ulmres  26353  ulmss  26362  pserdvlem2  26394  reeff1o  26413  reefiso  26414  reefgim  26416  recosf1o  26500  resinf1o  26501  relogcl  26540  logef  26546  logeftb  26548  logltb  26565  logcn  26612  advlog  26619  advlogexp  26620  logtayl  26625  logccv  26628  dvcxp1  26705  dvcncxp1  26708  cxpcn  26710  cxpcnOLD  26711  loglesqrt  26727  dvatan  26901  leibpi  26908  efrlim  26935  efrlimOLD  26936  amgmlem  26956  lgamgulmlem2  26996  lgamcvg2  27021  wilthlem3  27036  ftalem3  27041  mpodvdsmulf1o  27160  fsumdvdsmul  27161  dvdsmulf1o  27162  fsumdvdsmulOLD  27163  dchrelbas2  27204  dchrabs  27227  dchrisumlem1  27456  logdivsum  27500  log2sumbnd  27511  ostth2  27604  ostth  27606  ltsres  27630  nodense  27660  nolt02o  27663  nogt01o  27664  noetainflem4  27708  oniso  28267  bdayn0sf1o  28366  vtxdginducedm1lem3  29615  redwlk  29744  pthdivtx  29800  pthdlem1  29839  ex-fpar  30537  sspnval  30812  hhssnv  31339  hhssmetdval  31352  foresf1o  32579  1stpreimas  32785  cos9thpiminply  33945  xpinpreima  34063  xpinpreima2  34064  cnre2csqlem  34067  zzsnm  34116  cnzh  34125  rezh  34126  measres  34379  cntmeas  34383  cntnevol  34385  1stmbfm  34417  2ndmbfm  34418  carsggect  34475  omsmeas  34480  eulerpartgbij  34529  eulerpartlemgvv  34533  eulerpartlemgs2  34537  iwrdsplit  34544  fibp1  34558  coinfliplem  34636  coinflipprob  34637  gsumnunsn  34698  plyrecld  34706  signstres  34732  ftc2re  34755  bnj1253  35173  bnj1280  35176  f1resveqaeq  35241  noinfepregs  35289  gblacfnacd  35296  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem8  35392  txsconnlem  35434  cvmfolem  35473  cvmliftmolem1  35475  cvmliftlem6  35484  cvmliftlem7  35485  cvmliftlem9  35487  satfsucom  35548  satom  35550  satfvsucom  35551  satf0sucom  35567  mrsubff1  35708  msubff1  35750  dfrdg2  35987  funpartfv  36139  filnetlem4  36575  icoreunrn  37564  finixpnum  37806  poimirlem3  37824  poimirlem4  37825  poimirlem8  37829  poimirlem26  37847  poimirlem27  37848  itg2gt0cn  37876  areacirclem2  37910  areacirclem4  37912  sdclem2  37943  caures  37961  ismtyres  38009  diaintclN  41318  dibintclN  41427  dihintcl  41604  fsuppssindlem1  42834  imaiinfv  42935  mzpcompact2lem  42993  2rexfrabdioph  43038  3rexfrabdioph  43039  4rexfrabdioph  43040  6rexfrabdioph  43041  7rexfrabdioph  43042  jm2.27dlem1  43251  fnwe2lem2  43293  aomclem6  43301  deg1mhm  43442  hausgraph  43447  radcnvrat  44555  wessf1ornlem  45429  feqresmptf  45475  mccllem  45843  limcleqr  45888  limsupvaluz2  45982  supcnvlimsup  45984  limsupgtlem  46021  xlimconst2  46079  resincncf  46119  cncfperiod  46123  icccncfext  46131  cncfiooicclem1  46137  dvbdfbdioolem1  46172  dvnprodlem1  46190  dvnprodlem2  46191  itgioocnicc  46221  stoweidlem28  46272  fourierdlem18  46369  fourierdlem40  46391  fourierdlem42  46393  fourierdlem46  46396  fourierdlem51  46401  fourierdlem70  46420  fourierdlem71  46421  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem78  46428  fourierdlem80  46430  fourierdlem81  46431  fourierdlem82  46432  fourierdlem84  46434  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem92  46442  fourierdlem93  46443  fourierdlem94  46444  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  fourierdlem113  46463  sge0tsms  46624  sge0f1o  46626  sge0sup  46635  sge0less  46636  sge0ltfirp  46644  sge0resrnlem  46647  sge0resplit  46650  sge0le  46651  sge0split  46653  sge0fodjrnlem  46660  sge0iun  46663  meadjun  46706  meadjiunlem  46709  psmeasurelem  46714  caratheodory  46772  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  voncmpl  46865  mblvon  46883  smflimsuplem3  47066  cjnpoly  47135  afvres  47418  iccpartres  47664  iccelpart  47679  isubgredg  48112  isubgrgrim  48175  uhgrimisgrgric  48177  lincdifsn  48670  lindslinindimp2lem4  48707  lindslinindsimp2lem5  48708  lincresunit3lem2  48726  fdivmpt  48786  slotresfo  49144  basresposfo  49223  oppff1  49393  setrec2lem1  49938  setrecsres  49947  amgmwlem  50047