Theorem fvres 6691

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 3499	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5864	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 538	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6341	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6365	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6365	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2883	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   class class class wbr 5068   ↾ cres 5559  ℩cio 6314  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-xp 5563  df-res 5569  df-iota 6316  df-fv 6365

This theorem is referenced by:  fvresd  6692  funssfv  6693  fveqres  6714  feqresmpt  6736  dffv2  6758  fvreseq0  6810  respreima  6838  fveqressseq  6849  ffvresb  6890  fnressn  6922  fressnfv  6924  fvresi  6937  funfvima  6994  funiunfv  7009  soisores  7082  isores3  7090  isoini2  7094  ofres  7427  f1oweALT  7675  offres  7686  fo1stres  7717  fo2ndres  7718  fparlem1  7809  fparlem2  7810  fsplitfpar  7816  fo2ndf  7819  f1o2ndf1  7820  fnsuppres  7859  wfrlem4  7960  tfrlem1  8014  fr0g  8073  frsuc  8074  tz7.48lem  8079  seqomlem1  8088  seqomlem2  8089  seqomlem3  8090  seqomlem4  8091  onasuc  8155  onmsuc  8156  onesuc  8157  resixp  8499  fofinf1o  8801  ixpfi2  8824  updjudhcoinlf  9363  updjudhcoinrg  9364  updjud  9365  ackbij2lem2  9664  ackbij2lem3  9665  cfsmolem  9694  alephsing  9700  fpwwe2lem8  10061  inar1  10199  addpiord  10308  mulpiord  10309  fseq1p1m1  12984  injresinj  13161  seqfeq2  13396  seqres  13400  seqf1olem2  13413  hashgval  13696  hashinf  13698  hashgval2  13742  hashf1lem1  13816  pfxccat1  14066  shftidt  14443  climres  14934  fsumss  15084  isumclim3  15116  fsum2dlem  15127  ackbijnn  15185  fprodss  15304  fprod2dlem  15336  iprodclim3  15356  bpolylem  15404  fprodefsum  15450  reeff1  15475  bitsf1  15797  sadcadd  15809  sadadd2  15811  eucalgcvga  15932  eucalg  15933  unbenlem  16246  strfv2d  16531  setsid  16540  setsnid  16541  dmaf  17311  cdaf  17312  1stfcl  17449  2ndfcl  17450  resmhm  17987  resghm  18376  efgredlem  18875  gsumzaddlem  19043  dprdfadd  19144  dprdres  19152  dmdprdsplitlem  19161  dprdcntz2  19162  dmdprdsplit2lem  19169  dprdsplit  19172  dpjidcl  19182  ablfac1eu  19197  mgpf  19311  prdscrngd  19365  abvres  19612  reslmhm  19826  ltbwe  20255  subrgascl  20280  subrgasclcl  20281  znf1o  20700  znunithash  20713  smadiadetlem3  21279  lmres  21910  tx1cn  22219  tx2cn  22220  ptrescn  22249  cnmpt1st  22278  cnmpt2nd  22279  ptuncnv  22417  ptunhmeo  22418  cnextfres1  22678  prdstmdd  22734  prdsxmslem2  23141  subgnm2  23245  rescncf  23507  isncvsngp  23755  lmle  23906  ovoliunlem1  24105  ovolicc2lem4  24123  mblvol  24133  mbflimsup  24269  limcdif  24476  limcres  24486  dvres2lem  24510  dvlip  24592  dvlipcn  24593  dvlip2  24594  c1liplem1  24595  c1lip1  24596  c1lip3  24598  dvivthlem1  24607  lhop1lem  24612  lhop  24615  dvcvx  24619  ftc2ditglem  24644  itgsubstlem  24647  plyreres  24874  plyexmo  24904  aannenlem1  24919  taylthlem2  24964  ulmres  24978  ulmss  24987  pserdvlem2  25018  reeff1o  25037  reefiso  25038  reefgim  25040  recosf1o  25121  resinf1o  25122  relogcl  25161  logef  25167  logeftb  25169  logltb  25185  logcn  25232  advlog  25239  advlogexp  25240  logtayl  25245  logccv  25248  dvcxp1  25323  dvcncxp1  25326  cxpcn  25328  loglesqrt  25341  dvatan  25515  leibpi  25522  efrlim  25549  amgmlem  25569  lgamgulmlem2  25609  lgamcvg2  25634  wilthlem3  25649  ftalem3  25654  dvdsmulf1o  25773  fsumdvdsmul  25774  dchrelbas2  25815  dchrabs  25838  dchrisumlem1  26067  logdivsum  26111  log2sumbnd  26122  ostth2  26215  ostth  26217  vtxdginducedm1lem3  27325  redwlk  27456  pthdivtx  27512  pthdlem1  27549  ex-fpar  28243  sspnval  28516  hhssnv  29043  hhssmetdval  29056  foresf1o  30267  1stpreimas  30443  xpinpreima  31151  xpinpreima2  31152  cnre2csqlem  31155  rmulccn  31173  zzsnm  31204  cnzh  31213  rezh  31214  measres  31483  cntmeas  31487  cntnevol  31489  1stmbfm  31520  2ndmbfm  31521  carsggect  31578  omsmeas  31583  eulerpartgbij  31632  eulerpartlemgvv  31636  eulerpartlemgs2  31640  iwrdsplit  31647  fibp1  31661  coinfliplem  31738  coinflipprob  31739  gsumnunsn  31813  plyrecld  31821  signstres  31847  ftc2re  31871  bnj1253  32291  bnj1280  32294  f1resveqaeq  32360  subfacp1lem3  32431  subfacp1lem5  32433  erdszelem8  32447  txsconnlem  32489  cvmfolem  32528  cvmliftmolem1  32530  cvmliftlem6  32539  cvmliftlem7  32540  cvmliftlem9  32542  satfsucom  32603  satom  32605  satfvsucom  32606  satf0sucom  32622  mrsubff1  32763  msubff1  32805  fvresval  33012  dfrdg2  33042  sltres  33171  nodense  33198  nolt02o  33201  funpartfv  33408  filnetlem4  33731  icoreunrn  34642  finixpnum  34879  poimirlem3  34897  poimirlem4  34898  poimirlem8  34902  poimirlem26  34920  poimirlem27  34921  itg2gt0cn  34949  areacirclem2  34985  areacirclem4  34987  eqfnun  34999  sdclem2  35019  caures  35037  ismtyres  35088  diaintclN  38196  dibintclN  38305  dihintcl  38482  imaiinfv  39297  mzpcompact2lem  39355  2rexfrabdioph  39400  3rexfrabdioph  39401  4rexfrabdioph  39402  6rexfrabdioph  39403  7rexfrabdioph  39404  jm2.27dlem1  39613  fnwe2lem2  39658  aomclem6  39666  deg1mhm  39814  hausgraph  39819  radcnvrat  40653  wessf1ornlem  41452  feqresmptf  41506  mccllem  41885  limcleqr  41932  limsupvaluz2  42026  supcnvlimsup  42028  limsupgtlem  42065  xlimconst2  42123  resincncf  42165  cncfperiod  42169  icccncfext  42177  cncfiooicclem1  42183  dvbdfbdioolem1  42220  dvnprodlem1  42238  dvnprodlem2  42239  itgioocnicc  42269  stoweidlem28  42320  fourierdlem18  42417  fourierdlem40  42439  fourierdlem42  42441  fourierdlem46  42444  fourierdlem51  42449  fourierdlem70  42468  fourierdlem71  42469  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem78  42476  fourierdlem80  42478  fourierdlem81  42479  fourierdlem82  42480  fourierdlem84  42482  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem92  42490  fourierdlem93  42491  fourierdlem94  42492  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  fourierdlem112  42510  fourierdlem113  42511  sge0tsms  42669  sge0f1o  42671  sge0sup  42680  sge0less  42681  sge0ltfirp  42689  sge0resrnlem  42692  sge0resplit  42695  sge0le  42696  sge0split  42698  sge0fodjrnlem  42705  sge0iun  42708  meadjun  42751  meadjiunlem  42754  psmeasurelem  42759  caratheodory  42817  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvlelem4  42887  voncmpl  42910  mblvon  42928  smflimsuplem3  43103  afvres  43378  iccpartres  43585  iccelpart  43600  resmgmhm  44072  lincdifsn  44486  lindslinindimp2lem4  44523  lindslinindsimp2lem5  44524  lincresunit3lem2  44542  fdivmpt  44607  setrec2lem1  44803  setrecsres  44811  amgmwlem  44910