Theorem fvres 6877

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 3451	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5959	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6495	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6519	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6519	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2789	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   class class class wbr 5107   ↾ cres 5640  ℩cio 6462  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-res 5650  df-iota 6464  df-fv 6519

This theorem is referenced by:  fvresd  6878  funssfv  6879  fveqres  6905  feqresmpt  6930  dffv2  6956  eqfnun  7009  fvreseq0  7010  respreima  7038  fveqressseq  7051  ffvresb  7097  fnressn  7130  fressnfv  7132  fvresi  7147  funfvima  7204  funiunfv  7222  soisores  7302  isores3  7310  isoini2  7314  fvresval  7333  ofres  7672  f1oweALT  7951  offres  7962  fo1stres  7994  fo2ndres  7995  fparlem1  8091  fparlem2  8092  fsplitfpar  8097  fo2ndf  8100  f1o2ndf1  8101  fnsuppres  8170  tfrlem1  8344  fr0g  8404  frsuc  8405  tz7.48lem  8409  seqomlem1  8418  seqomlem2  8419  seqomlem3  8420  seqomlem4  8421  onasuc  8492  onmsuc  8493  onesuc  8494  resixp  8906  fofinf1o  9283  ixpfi2  9301  ttrclss  9673  updjudhcoinlf  9885  updjudhcoinrg  9886  updjud  9887  ackbij2lem2  10192  ackbij2lem3  10193  cfsmolem  10223  alephsing  10229  fpwwe2lem7  10590  inar1  10728  addpiord  10837  mulpiord  10838  fseq1p1m1  13559  injresinj  13749  seqfeq2  13990  seqres  13994  seqf1olem2  14007  hashgval  14298  hashinf  14300  hashgval2  14343  hashf1lem1  14420  pfxccat1  14667  shftidt  15048  climres  15541  fsumss  15691  isumclim3  15725  fsum2dlem  15736  ackbijnn  15794  fprodss  15914  fprod2dlem  15946  iprodclim3  15966  bpolylem  16014  fprodefsum  16061  reeff1  16088  bitsf1  16416  sadcadd  16428  sadadd2  16430  eucalgcvga  16556  eucalg  16557  unbenlem  16879  strfv2d  17171  setsid  17177  setsnid  17178  dfinito3  17967  dftermo3  17968  dmaf  18011  cdaf  18012  1stfcl  18158  2ndfcl  18159  resmgmhm  18638  resmhm  18747  resghm  19164  efgredlem  19677  gsumzaddlem  19851  dprdfadd  19952  dprdres  19960  dmdprdsplitlem  19969  dprdcntz2  19970  dmdprdsplit2lem  19977  dprdsplit  19980  dpjidcl  19990  ablfac1eu  20005  rngmgpf  20066  mgpf  20157  prdscrngd  20231  abvres  20740  reslmhm  20959  znf1o  21461  znunithash  21474  ltbwe  21951  subrgascl  21973  subrgasclcl  21974  smadiadetlem3  22555  lmres  23187  tx1cn  23496  tx2cn  23497  ptrescn  23526  cnmpt1st  23555  cnmpt2nd  23556  ptuncnv  23694  ptunhmeo  23695  cnextfres1  23955  prdstmdd  24011  prdsxmslem2  24417  subgnm2  24522  rescncf  24790  isncvsngp  25049  lmle  25201  ovoliunlem1  25403  ovolicc2lem4  25421  mblvol  25431  mbflimsup  25567  limcdif  25777  limcres  25787  dvres2lem  25811  dvlip  25898  dvlipcn  25899  dvlip2  25900  c1liplem1  25901  c1lip1  25902  c1lip3  25904  dvivthlem1  25913  lhop1lem  25918  lhop  25921  dvcvx  25925  ftc2ditglem  25952  itgsubstlem  25955  plyreres  26190  plyexmo  26221  aannenlem1  26236  taylthlem2  26282  taylthlem2OLD  26283  ulmres  26297  ulmss  26306  pserdvlem2  26338  reeff1o  26357  reefiso  26358  reefgim  26360  recosf1o  26444  resinf1o  26445  relogcl  26484  logef  26490  logeftb  26492  logltb  26509  logcn  26556  advlog  26563  advlogexp  26564  logtayl  26569  logccv  26572  dvcxp1  26649  dvcncxp1  26652  cxpcn  26654  cxpcnOLD  26655  loglesqrt  26671  dvatan  26845  leibpi  26852  efrlim  26879  efrlimOLD  26880  amgmlem  26900  lgamgulmlem2  26940  lgamcvg2  26965  wilthlem3  26980  ftalem3  26985  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  dchrelbas2  27148  dchrabs  27171  dchrisumlem1  27400  logdivsum  27444  log2sumbnd  27455  ostth2  27548  ostth  27550  sltres  27574  nodense  27604  nolt02o  27607  nogt01o  27608  noetainflem4  27652  onsiso  28169  bdayn0sf1o  28259  vtxdginducedm1lem3  29469  redwlk  29600  pthdivtx  29657  pthdlem1  29696  ex-fpar  30391  sspnval  30666  hhssnv  31193  hhssmetdval  31206  foresf1o  32433  1stpreimas  32629  cos9thpiminply  33778  xpinpreima  33896  xpinpreima2  33897  cnre2csqlem  33900  zzsnm  33949  cnzh  33958  rezh  33959  measres  34212  cntmeas  34216  cntnevol  34218  1stmbfm  34251  2ndmbfm  34252  carsggect  34309  omsmeas  34314  eulerpartgbij  34363  eulerpartlemgvv  34367  eulerpartlemgs2  34371  iwrdsplit  34378  fibp1  34392  coinfliplem  34470  coinflipprob  34471  gsumnunsn  34532  plyrecld  34540  signstres  34566  ftc2re  34589  bnj1253  35007  bnj1280  35010  f1resveqaeq  35075  gblacfnacd  35089  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem8  35185  txsconnlem  35227  cvmfolem  35266  cvmliftmolem1  35268  cvmliftlem6  35277  cvmliftlem7  35278  cvmliftlem9  35280  satfsucom  35341  satom  35343  satfvsucom  35344  satf0sucom  35360  mrsubff1  35501  msubff1  35543  dfrdg2  35783  funpartfv  35933  filnetlem4  36369  icoreunrn  37347  finixpnum  37599  poimirlem3  37617  poimirlem4  37618  poimirlem8  37622  poimirlem26  37640  poimirlem27  37641  itg2gt0cn  37669  areacirclem2  37703  areacirclem4  37705  sdclem2  37736  caures  37754  ismtyres  37802  diaintclN  41052  dibintclN  41161  dihintcl  41338  fsuppssindlem1  42579  imaiinfv  42681  mzpcompact2lem  42739  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  jm2.27dlem1  42998  fnwe2lem2  43040  aomclem6  43048  deg1mhm  43189  hausgraph  43194  radcnvrat  44303  wessf1ornlem  45179  feqresmptf  45225  mccllem  45595  limcleqr  45642  limsupvaluz2  45736  supcnvlimsup  45738  limsupgtlem  45775  xlimconst2  45833  resincncf  45873  cncfperiod  45877  icccncfext  45885  cncfiooicclem1  45891  dvbdfbdioolem1  45926  dvnprodlem1  45944  dvnprodlem2  45945  itgioocnicc  45975  stoweidlem28  46026  fourierdlem18  46123  fourierdlem40  46145  fourierdlem42  46147  fourierdlem46  46150  fourierdlem51  46155  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem78  46182  fourierdlem80  46184  fourierdlem81  46185  fourierdlem82  46186  fourierdlem84  46188  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem93  46197  fourierdlem94  46198  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  sge0tsms  46378  sge0f1o  46380  sge0sup  46389  sge0less  46390  sge0ltfirp  46398  sge0resrnlem  46401  sge0resplit  46404  sge0le  46405  sge0split  46407  sge0fodjrnlem  46414  sge0iun  46417  meadjun  46460  meadjiunlem  46463  psmeasurelem  46468  caratheodory  46526  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  voncmpl  46619  mblvon  46637  smflimsuplem3  46820  cjnpoly  46890  afvres  47173  iccpartres  47419  iccelpart  47434  isubgredg  47866  isubgrgrim  47929  uhgrimisgrgric  47931  lincdifsn  48413  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lincresunit3lem2  48469  fdivmpt  48529  slotresfo  48887  basresposfo  48966  oppff1  49137  setrec2lem1  49682  setrecsres  49691  amgmwlem  49791