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 3434	. . . . 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 2797	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   class class class wbr 5086   ↾ 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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  6983  fvreseq0  6984  respreima  7012  fveqressseq  7025  ffvresb  7072  fnressn  7105  fressnfv  7107  fvresi  7121  funfvima  7178  funiunfv  7196  soisores  7275  isores3  7283  isoini2  7287  fvresval  7306  ofres  7643  f1oweALT  7918  offres  7929  fo1stres  7961  fo2ndres  7962  fparlem1  8055  fparlem2  8056  fsplitfpar  8061  fo2ndf  8064  f1o2ndf1  8065  fnsuppres  8134  tfrlem1  8308  fr0g  8368  frsuc  8369  tz7.48lem  8373  seqomlem1  8382  seqomlem2  8383  seqomlem3  8384  seqomlem4  8385  onasuc  8456  onmsuc  8457  onesuc  8458  resixp  8874  fofinf1o  9235  ixpfi2  9253  ttrclss  9632  updjudhcoinlf  9847  updjudhcoinrg  9848  updjud  9849  ackbij2lem2  10152  ackbij2lem3  10153  cfsmolem  10183  alephsing  10189  fpwwe2lem7  10551  inar1  10689  addpiord  10798  mulpiord  10799  fseq1p1m1  13543  injresinj  13737  seqfeq2  13978  seqres  13982  seqf1olem2  13995  hashgval  14286  hashinf  14288  hashgval2  14331  hashf1lem1  14408  pfxccat1  14655  shftidt  15035  climres  15528  fsumss  15678  isumclim3  15712  fsum2dlem  15723  ackbijnn  15784  fprodss  15904  fprod2dlem  15936  iprodclim3  15956  bpolylem  16004  fprodefsum  16051  reeff1  16078  bitsf1  16406  sadcadd  16418  sadadd2  16420  eucalgcvga  16546  eucalg  16547  unbenlem  16870  strfv2d  17162  setsid  17168  setsnid  17169  dfinito3  17963  dftermo3  17964  dmaf  18007  cdaf  18008  1stfcl  18154  2ndfcl  18155  resmgmhm  18670  resmhm  18779  resghm  19198  efgredlem  19713  gsumzaddlem  19887  dprdfadd  19988  dprdres  19996  dmdprdsplitlem  20005  dprdcntz2  20006  dmdprdsplit2lem  20013  dprdsplit  20016  dpjidcl  20026  ablfac1eu  20041  rngmgpf  20129  mgpf  20220  prdscrngd  20292  abvres  20799  reslmhm  21039  znf1o  21541  znunithash  21554  ltbwe  22032  subrgascl  22054  subrgasclcl  22055  smadiadetlem3  22643  lmres  23275  tx1cn  23584  tx2cn  23585  ptrescn  23614  cnmpt1st  23643  cnmpt2nd  23644  ptuncnv  23782  ptunhmeo  23783  cnextfres1  24043  prdstmdd  24099  prdsxmslem2  24504  subgnm2  24609  rescncf  24874  isncvsngp  25126  lmle  25278  ovoliunlem1  25479  ovolicc2lem4  25497  mblvol  25507  mbflimsup  25643  limcdif  25853  limcres  25863  dvres2lem  25887  dvlip  25970  dvlipcn  25971  dvlip2  25972  c1liplem1  25973  c1lip1  25974  c1lip3  25976  dvivthlem1  25985  lhop1lem  25990  lhop  25993  dvcvx  25997  ftc2ditglem  26022  itgsubstlem  26025  plyreres  26259  plyexmo  26290  aannenlem1  26305  taylthlem2  26351  taylthlem2OLD  26352  ulmres  26366  ulmss  26375  pserdvlem2  26406  reeff1o  26425  reefiso  26426  reefgim  26428  recosf1o  26512  resinf1o  26513  relogcl  26552  logef  26558  logeftb  26560  logltb  26577  logcn  26624  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvcncxp1  26720  cxpcn  26722  loglesqrt  26738  dvatan  26912  leibpi  26919  efrlim  26946  efrlimOLD  26947  amgmlem  26967  lgamgulmlem2  27007  lgamcvg2  27032  wilthlem3  27047  ftalem3  27052  mpodvdsmulf1o  27171  fsumdvdsmul  27172  dvdsmulf1o  27173  dchrelbas2  27214  dchrabs  27237  dchrisumlem1  27466  logdivsum  27510  log2sumbnd  27521  ostth2  27614  ostth  27616  ltsres  27640  nodense  27670  nolt02o  27673  nogt01o  27674  noetainflem4  27718  oniso  28277  bdayn0sf1o  28376  vtxdginducedm1lem3  29625  redwlk  29754  pthdivtx  29810  pthdlem1  29849  ex-fpar  30547  sspnval  30823  hhssnv  31350  hhssmetdval  31363  foresf1o  32589  1stpreimas  32794  cos9thpiminply  33948  xpinpreima  34066  xpinpreima2  34067  cnre2csqlem  34070  zzsnm  34119  cnzh  34128  rezh  34129  measres  34382  cntmeas  34386  cntnevol  34388  1stmbfm  34420  2ndmbfm  34421  carsggect  34478  omsmeas  34483  eulerpartgbij  34532  eulerpartlemgvv  34536  eulerpartlemgs2  34540  iwrdsplit  34547  fibp1  34561  coinfliplem  34639  coinflipprob  34640  gsumnunsn  34701  plyrecld  34709  signstres  34735  ftc2re  34758  bnj1253  35175  bnj1280  35178  f1resveqaeq  35244  noinfepregs  35293  gblacfnacd  35300  subfacp1lem3  35380  subfacp1lem5  35382  erdszelem8  35396  txsconnlem  35438  cvmfolem  35477  cvmliftmolem1  35479  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem9  35491  satfsucom  35552  satom  35554  satfvsucom  35555  satf0sucom  35571  mrsubff1  35712  msubff1  35754  dfrdg2  35991  funpartfv  36143  filnetlem4  36579  icoreunrn  37689  finixpnum  37940  poimirlem3  37958  poimirlem4  37959  poimirlem8  37963  poimirlem26  37981  poimirlem27  37982  itg2gt0cn  38010  areacirclem2  38044  areacirclem4  38046  sdclem2  38077  caures  38095  ismtyres  38143  diaintclN  41518  dibintclN  41627  dihintcl  41804  fsuppssindlem1  43038  imaiinfv  43139  mzpcompact2lem  43197  2rexfrabdioph  43242  3rexfrabdioph  43243  4rexfrabdioph  43244  6rexfrabdioph  43245  7rexfrabdioph  43246  jm2.27dlem1  43455  fnwe2lem2  43497  aomclem6  43505  deg1mhm  43646  hausgraph  43651  radcnvrat  44759  wessf1ornlem  45633  feqresmptf  45678  mccllem  46045  limcleqr  46090  limsupvaluz2  46184  supcnvlimsup  46186  limsupgtlem  46223  xlimconst2  46281  resincncf  46321  cncfperiod  46325  icccncfext  46333  cncfiooicclem1  46339  dvbdfbdioolem1  46374  dvnprodlem1  46392  dvnprodlem2  46393  itgioocnicc  46423  stoweidlem28  46474  fourierdlem18  46571  fourierdlem40  46593  fourierdlem42  46595  fourierdlem46  46598  fourierdlem51  46603  fourierdlem70  46622  fourierdlem71  46623  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem78  46630  fourierdlem80  46632  fourierdlem81  46633  fourierdlem82  46634  fourierdlem84  46636  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem92  46644  fourierdlem93  46645  fourierdlem94  46646  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  sge0tsms  46826  sge0f1o  46828  sge0sup  46837  sge0less  46838  sge0ltfirp  46846  sge0resrnlem  46849  sge0resplit  46852  sge0le  46853  sge0split  46855  sge0fodjrnlem  46862  sge0iun  46865  meadjun  46908  meadjiunlem  46911  psmeasurelem  46916  caratheodory  46974  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  voncmpl  47067  mblvon  47085  smflimsuplem3  47268  cjnpoly  47349  afvres  47632  iccpartres  47890  iccelpart  47905  isubgredg  48354  isubgrgrim  48417  uhgrimisgrgric  48419  lincdifsn  48912  lindslinindimp2lem4  48949  lindslinindsimp2lem5  48950  lincresunit3lem2  48968  fdivmpt  49028  slotresfo  49386  basresposfo  49465  oppff1  49635  setrec2lem1  50180  setrecsres  50189  amgmwlem  50289