Theorem fvres 6854

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 3445	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5948	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6477	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6501	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6501	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2797	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   class class class wbr 5099   ↾ cres 5627  ℩cio 6447  ‘cfv 6493

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 5242  ax-nul 5252  ax-pr 5378

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-xp 5631  df-res 5637  df-iota 6449  df-fv 6501

This theorem is referenced by:  fvresd  6855  funssfv  6856  fveqres  6879  feqresmpt  6904  dffv2  6930  eqfnun  6984  fvreseq0  6985  respreima  7013  fveqressseq  7026  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  8056  fparlem2  8057  fsplitfpar  8062  fo2ndf  8065  f1o2ndf1  8066  fnsuppres  8135  tfrlem1  8309  fr0g  8369  frsuc  8370  tz7.48lem  8374  seqomlem1  8383  seqomlem2  8384  seqomlem3  8385  seqomlem4  8386  onasuc  8457  onmsuc  8458  onesuc  8459  resixp  8875  fofinf1o  9236  ixpfi2  9254  ttrclss  9633  updjudhcoinlf  9848  updjudhcoinrg  9849  updjud  9850  ackbij2lem2  10153  ackbij2lem3  10154  cfsmolem  10184  alephsing  10190  fpwwe2lem7  10552  inar1  10690  addpiord  10799  mulpiord  10800  fseq1p1m1  13518  injresinj  13711  seqfeq2  13952  seqres  13956  seqf1olem2  13969  hashgval  14260  hashinf  14262  hashgval2  14305  hashf1lem1  14382  pfxccat1  14629  shftidt  15009  climres  15502  fsumss  15652  isumclim3  15686  fsum2dlem  15697  ackbijnn  15755  fprodss  15875  fprod2dlem  15907  iprodclim3  15927  bpolylem  15975  fprodefsum  16022  reeff1  16049  bitsf1  16377  sadcadd  16389  sadadd2  16391  eucalgcvga  16517  eucalg  16518  unbenlem  16840  strfv2d  17132  setsid  17138  setsnid  17139  dfinito3  17933  dftermo3  17934  dmaf  17977  cdaf  17978  1stfcl  18124  2ndfcl  18125  resmgmhm  18640  resmhm  18749  resghm  19165  efgredlem  19680  gsumzaddlem  19854  dprdfadd  19955  dprdres  19963  dmdprdsplitlem  19972  dprdcntz2  19973  dmdprdsplit2lem  19980  dprdsplit  19983  dpjidcl  19993  ablfac1eu  20008  rngmgpf  20096  mgpf  20187  prdscrngd  20261  abvres  20768  reslmhm  21008  znf1o  21510  znunithash  21523  ltbwe  22003  subrgascl  22025  subrgasclcl  22026  smadiadetlem3  22616  lmres  23248  tx1cn  23557  tx2cn  23558  ptrescn  23587  cnmpt1st  23616  cnmpt2nd  23617  ptuncnv  23755  ptunhmeo  23756  cnextfres1  24016  prdstmdd  24072  prdsxmslem2  24477  subgnm2  24582  rescncf  24850  isncvsngp  25109  lmle  25261  ovoliunlem1  25463  ovolicc2lem4  25481  mblvol  25491  mbflimsup  25627  limcdif  25837  limcres  25847  dvres2lem  25871  dvlip  25958  dvlipcn  25959  dvlip2  25960  c1liplem1  25961  c1lip1  25962  c1lip3  25964  dvivthlem1  25973  lhop1lem  25978  lhop  25981  dvcvx  25985  ftc2ditglem  26012  itgsubstlem  26015  plyreres  26250  plyexmo  26281  aannenlem1  26296  taylthlem2  26342  taylthlem2OLD  26343  ulmres  26357  ulmss  26366  pserdvlem2  26398  reeff1o  26417  reefiso  26418  reefgim  26420  recosf1o  26504  resinf1o  26505  relogcl  26544  logef  26550  logeftb  26552  logltb  26569  logcn  26616  advlog  26623  advlogexp  26624  logtayl  26629  logccv  26632  dvcxp1  26709  dvcncxp1  26712  cxpcn  26714  cxpcnOLD  26715  loglesqrt  26731  dvatan  26905  leibpi  26912  efrlim  26939  efrlimOLD  26940  amgmlem  26960  lgamgulmlem2  27000  lgamcvg2  27025  wilthlem3  27040  ftalem3  27045  mpodvdsmulf1o  27164  fsumdvdsmul  27165  dvdsmulf1o  27166  fsumdvdsmulOLD  27167  dchrelbas2  27208  dchrabs  27231  dchrisumlem1  27460  logdivsum  27504  log2sumbnd  27515  ostth2  27608  ostth  27610  sltres  27634  nodense  27664  nolt02o  27667  nogt01o  27668  noetainflem4  27712  onsiso  28252  bdayn0sf1o  28349  vtxdginducedm1lem3  29598  redwlk  29727  pthdivtx  29783  pthdlem1  29822  ex-fpar  30520  sspnval  30795  hhssnv  31322  hhssmetdval  31335  foresf1o  32561  1stpreimas  32766  cos9thpiminply  33926  xpinpreima  34044  xpinpreima2  34045  cnre2csqlem  34048  zzsnm  34097  cnzh  34106  rezh  34107  measres  34360  cntmeas  34364  cntnevol  34366  1stmbfm  34398  2ndmbfm  34399  carsggect  34456  omsmeas  34461  eulerpartgbij  34510  eulerpartlemgvv  34514  eulerpartlemgs2  34518  iwrdsplit  34525  fibp1  34539  coinfliplem  34617  coinflipprob  34618  gsumnunsn  34679  plyrecld  34687  signstres  34713  ftc2re  34736  bnj1253  35154  bnj1280  35157  f1resveqaeq  35222  noinfepregs  35270  gblacfnacd  35277  subfacp1lem3  35357  subfacp1lem5  35359  erdszelem8  35373  txsconnlem  35415  cvmfolem  35454  cvmliftmolem1  35456  cvmliftlem6  35465  cvmliftlem7  35466  cvmliftlem9  35468  satfsucom  35529  satom  35531  satfvsucom  35532  satf0sucom  35548  mrsubff1  35689  msubff1  35731  dfrdg2  35968  funpartfv  36120  filnetlem4  36556  icoreunrn  37535  finixpnum  37777  poimirlem3  37795  poimirlem4  37796  poimirlem8  37800  poimirlem26  37818  poimirlem27  37819  itg2gt0cn  37847  areacirclem2  37881  areacirclem4  37883  sdclem2  37914  caures  37932  ismtyres  37980  diaintclN  41355  dibintclN  41464  dihintcl  41641  fsuppssindlem1  42870  imaiinfv  42971  mzpcompact2lem  43029  2rexfrabdioph  43074  3rexfrabdioph  43075  4rexfrabdioph  43076  6rexfrabdioph  43077  7rexfrabdioph  43078  jm2.27dlem1  43287  fnwe2lem2  43329  aomclem6  43337  deg1mhm  43478  hausgraph  43483  radcnvrat  44591  wessf1ornlem  45465  feqresmptf  45511  mccllem  45879  limcleqr  45924  limsupvaluz2  46018  supcnvlimsup  46020  limsupgtlem  46057  xlimconst2  46115  resincncf  46155  cncfperiod  46159  icccncfext  46167  cncfiooicclem1  46173  dvbdfbdioolem1  46208  dvnprodlem1  46226  dvnprodlem2  46227  itgioocnicc  46257  stoweidlem28  46308  fourierdlem18  46405  fourierdlem40  46427  fourierdlem42  46429  fourierdlem46  46432  fourierdlem51  46437  fourierdlem70  46456  fourierdlem71  46457  fourierdlem73  46459  fourierdlem74  46460  fourierdlem75  46461  fourierdlem76  46462  fourierdlem78  46464  fourierdlem80  46466  fourierdlem81  46467  fourierdlem82  46468  fourierdlem84  46470  fourierdlem89  46475  fourierdlem90  46476  fourierdlem91  46477  fourierdlem92  46478  fourierdlem93  46479  fourierdlem94  46480  fourierdlem101  46487  fourierdlem103  46489  fourierdlem104  46490  fourierdlem111  46497  fourierdlem112  46498  fourierdlem113  46499  sge0tsms  46660  sge0f1o  46662  sge0sup  46671  sge0less  46672  sge0ltfirp  46680  sge0resrnlem  46683  sge0resplit  46686  sge0le  46687  sge0split  46689  sge0fodjrnlem  46696  sge0iun  46699  meadjun  46742  meadjiunlem  46745  psmeasurelem  46750  caratheodory  46808  hoidmvlelem2  46876  hoidmvlelem3  46877  hoidmvlelem4  46878  voncmpl  46901  mblvon  46919  smflimsuplem3  47102  cjnpoly  47171  afvres  47454  iccpartres  47700  iccelpart  47715  isubgredg  48148  isubgrgrim  48211  uhgrimisgrgric  48213  lincdifsn  48706  lindslinindimp2lem4  48743  lindslinindsimp2lem5  48744  lincresunit3lem2  48762  fdivmpt  48822  slotresfo  49180  basresposfo  49259  oppff1  49429  setrec2lem1  49974  setrecsres  49983  amgmwlem  50083