Theorem fvres 6859

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   class class class wbr 5085   ↾ cres 5633  ℩cio 6452  ‘cfv 6498

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-res 5643  df-iota 6454  df-fv 6506

This theorem is referenced by:  fvresd  6860  funssfv  6861  fveqres  6884  feqresmpt  6909  dffv2  6935  eqfnun  6989  fvreseq0  6990  respreima  7018  fveqressseq  7031  ffvresb  7078  fnressn  7112  fressnfv  7114  fvresi  7128  funfvima  7185  funiunfv  7203  soisores  7282  isores3  7290  isoini2  7294  fvresval  7313  ofres  7650  f1oweALT  7925  offres  7936  fo1stres  7968  fo2ndres  7969  fparlem1  8062  fparlem2  8063  fsplitfpar  8068  fo2ndf  8071  f1o2ndf1  8072  fnsuppres  8141  tfrlem1  8315  fr0g  8375  frsuc  8376  tz7.48lem  8380  seqomlem1  8389  seqomlem2  8390  seqomlem3  8391  seqomlem4  8392  onasuc  8463  onmsuc  8464  onesuc  8465  resixp  8881  fofinf1o  9242  ixpfi2  9260  ttrclss  9641  updjudhcoinlf  9856  updjudhcoinrg  9857  updjud  9858  ackbij2lem2  10161  ackbij2lem3  10162  cfsmolem  10192  alephsing  10198  fpwwe2lem7  10560  inar1  10698  addpiord  10807  mulpiord  10808  fseq1p1m1  13552  injresinj  13746  seqfeq2  13987  seqres  13991  seqf1olem2  14004  hashgval  14295  hashinf  14297  hashgval2  14340  hashf1lem1  14417  pfxccat1  14664  shftidt  15044  climres  15537  fsumss  15687  isumclim3  15721  fsum2dlem  15732  ackbijnn  15793  fprodss  15913  fprod2dlem  15945  iprodclim3  15965  bpolylem  16013  fprodefsum  16060  reeff1  16087  bitsf1  16415  sadcadd  16427  sadadd2  16429  eucalgcvga  16555  eucalg  16556  unbenlem  16879  strfv2d  17171  setsid  17177  setsnid  17178  dfinito3  17972  dftermo3  17973  dmaf  18016  cdaf  18017  1stfcl  18163  2ndfcl  18164  resmgmhm  18679  resmhm  18788  resghm  19207  efgredlem  19722  gsumzaddlem  19896  dprdfadd  19997  dprdres  20005  dmdprdsplitlem  20014  dprdcntz2  20015  dmdprdsplit2lem  20022  dprdsplit  20025  dpjidcl  20035  ablfac1eu  20050  rngmgpf  20138  mgpf  20229  prdscrngd  20301  abvres  20808  reslmhm  21047  znf1o  21531  znunithash  21544  ltbwe  22022  subrgascl  22044  subrgasclcl  22045  smadiadetlem3  22633  lmres  23265  tx1cn  23574  tx2cn  23575  ptrescn  23604  cnmpt1st  23633  cnmpt2nd  23634  ptuncnv  23772  ptunhmeo  23773  cnextfres1  24033  prdstmdd  24089  prdsxmslem2  24494  subgnm2  24599  rescncf  24864  isncvsngp  25116  lmle  25268  ovoliunlem1  25469  ovolicc2lem4  25487  mblvol  25497  mbflimsup  25633  limcdif  25843  limcres  25853  dvres2lem  25877  dvlip  25960  dvlipcn  25961  dvlip2  25962  c1liplem1  25963  c1lip1  25964  c1lip3  25966  dvivthlem1  25975  lhop1lem  25980  lhop  25983  dvcvx  25987  ftc2ditglem  26012  itgsubstlem  26015  plyreres  26249  plyexmo  26279  aannenlem1  26294  taylthlem2  26339  ulmres  26353  ulmss  26362  pserdvlem2  26393  reeff1o  26412  reefiso  26413  reefgim  26415  recosf1o  26499  resinf1o  26500  relogcl  26539  logef  26545  logeftb  26547  logltb  26564  logcn  26611  advlog  26618  advlogexp  26619  logtayl  26624  logccv  26627  dvcxp1  26704  dvcncxp1  26707  cxpcn  26709  loglesqrt  26725  dvatan  26899  leibpi  26906  efrlim  26933  amgmlem  26953  lgamgulmlem2  26993  lgamcvg2  27018  wilthlem3  27033  ftalem3  27038  mpodvdsmulf1o  27157  fsumdvdsmul  27158  dvdsmulf1o  27159  dchrelbas2  27200  dchrabs  27223  dchrisumlem1  27452  logdivsum  27496  log2sumbnd  27507  ostth2  27600  ostth  27602  ltsres  27626  nodense  27656  nolt02o  27659  nogt01o  27660  noetainflem4  27704  oniso  28263  bdayn0sf1o  28362  vtxdginducedm1lem3  29610  redwlk  29739  pthdivtx  29795  pthdlem1  29834  ex-fpar  30532  sspnval  30808  hhssnv  31335  hhssmetdval  31348  foresf1o  32574  1stpreimas  32779  cos9thpiminply  33932  xpinpreima  34050  xpinpreima2  34051  cnre2csqlem  34054  zzsnm  34103  cnzh  34112  rezh  34113  measres  34366  cntmeas  34370  cntnevol  34372  1stmbfm  34404  2ndmbfm  34405  carsggect  34462  omsmeas  34467  eulerpartgbij  34516  eulerpartlemgvv  34520  eulerpartlemgs2  34524  iwrdsplit  34531  fibp1  34545  coinfliplem  34623  coinflipprob  34624  gsumnunsn  34685  plyrecld  34693  signstres  34719  ftc2re  34742  bnj1253  35159  bnj1280  35162  f1resveqaeq  35228  noinfepregs  35277  gblacfnacd  35284  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem8  35380  txsconnlem  35422  cvmfolem  35461  cvmliftmolem1  35463  cvmliftlem6  35472  cvmliftlem7  35473  cvmliftlem9  35475  satfsucom  35536  satom  35538  satfvsucom  35539  satf0sucom  35555  mrsubff1  35696  msubff1  35738  dfrdg2  35975  funpartfv  36127  filnetlem4  36563  icoreunrn  37675  finixpnum  37926  poimirlem3  37944  poimirlem4  37945  poimirlem8  37949  poimirlem26  37967  poimirlem27  37968  itg2gt0cn  37996  areacirclem2  38030  areacirclem4  38032  sdclem2  38063  caures  38081  ismtyres  38129  diaintclN  41504  dibintclN  41613  dihintcl  41790  fsuppssindlem1  43024  imaiinfv  43125  mzpcompact2lem  43183  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  jm2.27dlem1  43437  fnwe2lem2  43479  aomclem6  43487  deg1mhm  43628  hausgraph  43633  radcnvrat  44741  wessf1ornlem  45615  feqresmptf  45660  mccllem  46027  limcleqr  46072  limsupvaluz2  46166  supcnvlimsup  46168  limsupgtlem  46205  xlimconst2  46263  resincncf  46303  cncfperiod  46307  icccncfext  46315  cncfiooicclem1  46321  dvbdfbdioolem1  46356  dvnprodlem1  46374  dvnprodlem2  46375  itgioocnicc  46405  stoweidlem28  46456  fourierdlem18  46553  fourierdlem40  46575  fourierdlem42  46577  fourierdlem46  46580  fourierdlem51  46585  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem80  46614  fourierdlem81  46615  fourierdlem82  46616  fourierdlem84  46618  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem94  46628  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  sge0tsms  46808  sge0f1o  46810  sge0sup  46819  sge0less  46820  sge0ltfirp  46828  sge0resrnlem  46831  sge0resplit  46834  sge0le  46835  sge0split  46837  sge0fodjrnlem  46844  sge0iun  46847  meadjun  46890  meadjiunlem  46893  psmeasurelem  46898  caratheodory  46956  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  voncmpl  47049  mblvon  47067  smflimsuplem3  47250  cjnpoly  47337  afvres  47620  iccpartres  47878  iccelpart  47893  isubgredg  48342  isubgrgrim  48405  uhgrimisgrgric  48407  lincdifsn  48900  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  lincresunit3lem2  48956  fdivmpt  49016  slotresfo  49374  basresposfo  49453  oppff1  49623  setrec2lem1  50168  setrecsres  50177  amgmwlem  50277