Theorem fvres 6775

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 3426	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5889	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6402	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6426	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6426	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2804	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   class class class wbr 5070   ↾ cres 5582  ℩cio 6374  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-res 5592  df-iota 6376  df-fv 6426

This theorem is referenced by:  fvresd  6776  funssfv  6777  fveqres  6798  feqresmpt  6820  dffv2  6845  fvreseq0  6897  respreima  6925  fveqressseq  6939  ffvresb  6980  fnressn  7012  fressnfv  7014  fvresi  7027  funfvima  7088  funiunfv  7103  soisores  7178  isores3  7186  isoini2  7190  ofres  7530  f1oweALT  7788  offres  7799  fo1stres  7830  fo2ndres  7831  fparlem1  7923  fparlem2  7924  fsplitfpar  7930  fo2ndf  7933  f1o2ndf1  7934  fnsuppres  7978  wfrlem4OLD  8114  tfrlem1  8178  fr0g  8237  frsuc  8238  tz7.48lem  8242  seqomlem1  8251  seqomlem2  8252  seqomlem3  8253  seqomlem4  8254  onasuc  8320  onmsuc  8321  onesuc  8322  resixp  8679  fofinf1o  9024  ixpfi2  9047  updjudhcoinlf  9621  updjudhcoinrg  9622  updjud  9623  ackbij2lem2  9927  ackbij2lem3  9928  cfsmolem  9957  alephsing  9963  fpwwe2lem7  10324  inar1  10462  addpiord  10571  mulpiord  10572  fseq1p1m1  13259  injresinj  13436  seqfeq2  13674  seqres  13678  seqf1olem2  13691  hashgval  13975  hashinf  13977  hashgval2  14021  hashf1lem1  14096  hashf1lem1OLD  14097  pfxccat1  14343  shftidt  14721  climres  15212  fsumss  15365  isumclim3  15399  fsum2dlem  15410  ackbijnn  15468  fprodss  15586  fprod2dlem  15618  iprodclim3  15638  bpolylem  15686  fprodefsum  15732  reeff1  15757  bitsf1  16081  sadcadd  16093  sadadd2  16095  eucalgcvga  16219  eucalg  16220  unbenlem  16537  strfv2d  16831  setsid  16837  setsnid  16838  setsnidOLD  16839  dfinito3  17636  dftermo3  17637  dmaf  17680  cdaf  17681  1stfcl  17830  2ndfcl  17831  resmhm  18374  resghm  18765  efgredlem  19268  gsumzaddlem  19437  dprdfadd  19538  dprdres  19546  dmdprdsplitlem  19555  dprdcntz2  19556  dmdprdsplit2lem  19563  dprdsplit  19566  dpjidcl  19576  ablfac1eu  19591  mgpf  19713  prdscrngd  19767  abvres  20014  reslmhm  20229  znf1o  20671  znunithash  20684  ltbwe  21155  subrgascl  21184  subrgasclcl  21185  smadiadetlem3  21725  lmres  22359  tx1cn  22668  tx2cn  22669  ptrescn  22698  cnmpt1st  22727  cnmpt2nd  22728  ptuncnv  22866  ptunhmeo  22867  cnextfres1  23127  prdstmdd  23183  prdsxmslem2  23591  subgnm2  23696  rescncf  23966  isncvsngp  24218  lmle  24370  ovoliunlem1  24571  ovolicc2lem4  24589  mblvol  24599  mbflimsup  24735  limcdif  24945  limcres  24955  dvres2lem  24979  dvlip  25062  dvlipcn  25063  dvlip2  25064  c1liplem1  25065  c1lip1  25066  c1lip3  25068  dvivthlem1  25077  lhop1lem  25082  lhop  25085  dvcvx  25089  ftc2ditglem  25114  itgsubstlem  25117  plyreres  25348  plyexmo  25378  aannenlem1  25393  taylthlem2  25438  ulmres  25452  ulmss  25461  pserdvlem2  25492  reeff1o  25511  reefiso  25512  reefgim  25514  recosf1o  25596  resinf1o  25597  relogcl  25636  logef  25642  logeftb  25644  logltb  25660  logcn  25707  advlog  25714  advlogexp  25715  logtayl  25720  logccv  25723  dvcxp1  25798  dvcncxp1  25801  cxpcn  25803  loglesqrt  25816  dvatan  25990  leibpi  25997  efrlim  26024  amgmlem  26044  lgamgulmlem2  26084  lgamcvg2  26109  wilthlem3  26124  ftalem3  26129  dvdsmulf1o  26248  fsumdvdsmul  26249  dchrelbas2  26290  dchrabs  26313  dchrisumlem1  26542  logdivsum  26586  log2sumbnd  26597  ostth2  26690  ostth  26692  vtxdginducedm1lem3  27811  redwlk  27942  pthdivtx  27998  pthdlem1  28035  ex-fpar  28727  sspnval  29000  hhssnv  29527  hhssmetdval  29540  foresf1o  30751  1stpreimas  30940  xpinpreima  31758  xpinpreima2  31759  cnre2csqlem  31762  rmulccn  31780  zzsnm  31811  cnzh  31820  rezh  31821  measres  32090  cntmeas  32094  cntnevol  32096  1stmbfm  32127  2ndmbfm  32128  carsggect  32185  omsmeas  32190  eulerpartgbij  32239  eulerpartlemgvv  32243  eulerpartlemgs2  32247  iwrdsplit  32254  fibp1  32268  coinfliplem  32345  coinflipprob  32346  gsumnunsn  32420  plyrecld  32428  signstres  32454  ftc2re  32478  bnj1253  32897  bnj1280  32900  f1resveqaeq  32957  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem8  33060  txsconnlem  33102  cvmfolem  33141  cvmliftmolem1  33143  cvmliftlem6  33152  cvmliftlem7  33153  cvmliftlem9  33155  satfsucom  33216  satom  33218  satfvsucom  33219  satf0sucom  33235  mrsubff1  33376  msubff1  33418  fvresval  33647  dfrdg2  33677  ttrclss  33706  sltres  33792  nodense  33822  nolt02o  33825  nogt01o  33826  noetainflem4  33870  funpartfv  34174  filnetlem4  34497  icoreunrn  35457  finixpnum  35689  poimirlem3  35707  poimirlem4  35708  poimirlem8  35712  poimirlem26  35730  poimirlem27  35731  itg2gt0cn  35759  areacirclem2  35793  areacirclem4  35795  eqfnun  35807  sdclem2  35827  caures  35845  ismtyres  35893  diaintclN  38999  dibintclN  39108  dihintcl  39285  fsuppssindlem1  40203  imaiinfv  40431  mzpcompact2lem  40489  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  jm2.27dlem1  40747  fnwe2lem2  40792  aomclem6  40800  deg1mhm  40948  hausgraph  40953  radcnvrat  41821  wessf1ornlem  42611  feqresmptf  42661  mccllem  43028  limcleqr  43075  limsupvaluz2  43169  supcnvlimsup  43171  limsupgtlem  43208  xlimconst2  43266  resincncf  43306  cncfperiod  43310  icccncfext  43318  cncfiooicclem1  43324  dvbdfbdioolem1  43359  dvnprodlem1  43377  dvnprodlem2  43378  itgioocnicc  43408  stoweidlem28  43459  fourierdlem18  43556  fourierdlem40  43578  fourierdlem42  43580  fourierdlem46  43583  fourierdlem51  43588  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem78  43615  fourierdlem80  43617  fourierdlem81  43618  fourierdlem82  43619  fourierdlem84  43621  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem93  43630  fourierdlem94  43631  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  sge0tsms  43808  sge0f1o  43810  sge0sup  43819  sge0less  43820  sge0ltfirp  43828  sge0resrnlem  43831  sge0resplit  43834  sge0le  43835  sge0split  43837  sge0fodjrnlem  43844  sge0iun  43847  meadjun  43890  meadjiunlem  43893  psmeasurelem  43898  caratheodory  43956  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  voncmpl  44049  mblvon  44067  smflimsuplem3  44242  afvres  44551  iccpartres  44758  iccelpart  44773  resmgmhm  45240  lincdifsn  45653  lindslinindimp2lem4  45690  lindslinindsimp2lem5  45691  lincresunit3lem2  45709  fdivmpt  45774  setrec2lem1  46285  setrecsres  46293  amgmwlem  46392