Theorem fvres 6894

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 3463	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5975	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6514	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6538	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6538	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2795	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   class class class wbr 5119   ↾ cres 5656  ℩cio 6481  ‘cfv 6530

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-res 5666  df-iota 6483  df-fv 6538

This theorem is referenced by:  fvresd  6895  funssfv  6896  fveqres  6922  feqresmpt  6947  dffv2  6973  eqfnun  7026  fvreseq0  7027  respreima  7055  fveqressseq  7068  ffvresb  7114  fnressn  7147  fressnfv  7149  fvresi  7164  funfvima  7221  funiunfv  7239  soisores  7319  isores3  7327  isoini2  7331  fvresval  7350  ofres  7688  f1oweALT  7969  offres  7980  fo1stres  8012  fo2ndres  8013  fparlem1  8109  fparlem2  8110  fsplitfpar  8115  fo2ndf  8118  f1o2ndf1  8119  fnsuppres  8188  wfrlem4OLD  8324  tfrlem1  8388  fr0g  8448  frsuc  8449  tz7.48lem  8453  seqomlem1  8462  seqomlem2  8463  seqomlem3  8464  seqomlem4  8465  onasuc  8538  onmsuc  8539  onesuc  8540  resixp  8945  fofinf1o  9342  ixpfi2  9360  ttrclss  9732  updjudhcoinlf  9944  updjudhcoinrg  9945  updjud  9946  ackbij2lem2  10251  ackbij2lem3  10252  cfsmolem  10282  alephsing  10288  fpwwe2lem7  10649  inar1  10787  addpiord  10896  mulpiord  10897  fseq1p1m1  13613  injresinj  13802  seqfeq2  14041  seqres  14045  seqf1olem2  14058  hashgval  14349  hashinf  14351  hashgval2  14394  hashf1lem1  14471  pfxccat1  14718  shftidt  15099  climres  15589  fsumss  15739  isumclim3  15773  fsum2dlem  15784  ackbijnn  15842  fprodss  15962  fprod2dlem  15994  iprodclim3  16014  bpolylem  16062  fprodefsum  16109  reeff1  16136  bitsf1  16463  sadcadd  16475  sadadd2  16477  eucalgcvga  16603  eucalg  16604  unbenlem  16926  strfv2d  17218  setsid  17224  setsnid  17225  dfinito3  18016  dftermo3  18017  dmaf  18060  cdaf  18061  1stfcl  18207  2ndfcl  18208  resmgmhm  18687  resmhm  18796  resghm  19213  efgredlem  19726  gsumzaddlem  19900  dprdfadd  20001  dprdres  20009  dmdprdsplitlem  20018  dprdcntz2  20019  dmdprdsplit2lem  20026  dprdsplit  20029  dpjidcl  20039  ablfac1eu  20054  rngmgpf  20115  mgpf  20206  prdscrngd  20280  abvres  20789  reslmhm  21008  znf1o  21510  znunithash  21523  ltbwe  22000  subrgascl  22022  subrgasclcl  22023  smadiadetlem3  22604  lmres  23236  tx1cn  23545  tx2cn  23546  ptrescn  23575  cnmpt1st  23604  cnmpt2nd  23605  ptuncnv  23743  ptunhmeo  23744  cnextfres1  24004  prdstmdd  24060  prdsxmslem2  24466  subgnm2  24571  rescncf  24839  isncvsngp  25099  lmle  25251  ovoliunlem1  25453  ovolicc2lem4  25471  mblvol  25481  mbflimsup  25617  limcdif  25827  limcres  25837  dvres2lem  25861  dvlip  25948  dvlipcn  25949  dvlip2  25950  c1liplem1  25951  c1lip1  25952  c1lip3  25954  dvivthlem1  25963  lhop1lem  25968  lhop  25971  dvcvx  25975  ftc2ditglem  26002  itgsubstlem  26005  plyreres  26240  plyexmo  26271  aannenlem1  26286  taylthlem2  26332  taylthlem2OLD  26333  ulmres  26347  ulmss  26356  pserdvlem2  26388  reeff1o  26407  reefiso  26408  reefgim  26410  recosf1o  26494  resinf1o  26495  relogcl  26534  logef  26540  logeftb  26542  logltb  26559  logcn  26606  advlog  26613  advlogexp  26614  logtayl  26619  logccv  26622  dvcxp1  26699  dvcncxp1  26702  cxpcn  26704  cxpcnOLD  26705  loglesqrt  26721  dvatan  26895  leibpi  26902  efrlim  26929  efrlimOLD  26930  amgmlem  26950  lgamgulmlem2  26990  lgamcvg2  27015  wilthlem3  27030  ftalem3  27035  mpodvdsmulf1o  27154  fsumdvdsmul  27155  dvdsmulf1o  27156  fsumdvdsmulOLD  27157  dchrelbas2  27198  dchrabs  27221  dchrisumlem1  27450  logdivsum  27494  log2sumbnd  27505  ostth2  27598  ostth  27600  sltres  27624  nodense  27654  nolt02o  27657  nogt01o  27658  noetainflem4  27702  vtxdginducedm1lem3  29467  redwlk  29598  pthdivtx  29655  pthdlem1  29694  ex-fpar  30389  sspnval  30664  hhssnv  31191  hhssmetdval  31204  foresf1o  32431  1stpreimas  32629  cos9thpiminply  33768  xpinpreima  33883  xpinpreima2  33884  cnre2csqlem  33887  zzsnm  33936  cnzh  33945  rezh  33946  measres  34199  cntmeas  34203  cntnevol  34205  1stmbfm  34238  2ndmbfm  34239  carsggect  34296  omsmeas  34301  eulerpartgbij  34350  eulerpartlemgvv  34354  eulerpartlemgs2  34358  iwrdsplit  34365  fibp1  34379  coinfliplem  34457  coinflipprob  34458  gsumnunsn  34519  plyrecld  34527  signstres  34553  ftc2re  34576  bnj1253  34994  bnj1280  34997  f1resveqaeq  35062  gblacfnacd  35076  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem8  35166  txsconnlem  35208  cvmfolem  35247  cvmliftmolem1  35249  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem9  35261  satfsucom  35322  satom  35324  satfvsucom  35325  satf0sucom  35341  mrsubff1  35482  msubff1  35524  dfrdg2  35759  funpartfv  35909  filnetlem4  36345  icoreunrn  37323  finixpnum  37575  poimirlem3  37593  poimirlem4  37594  poimirlem8  37598  poimirlem26  37616  poimirlem27  37617  itg2gt0cn  37645  areacirclem2  37679  areacirclem4  37681  sdclem2  37712  caures  37730  ismtyres  37778  diaintclN  41023  dibintclN  41132  dihintcl  41309  fsuppssindlem1  42561  imaiinfv  42663  mzpcompact2lem  42721  2rexfrabdioph  42766  3rexfrabdioph  42767  4rexfrabdioph  42768  6rexfrabdioph  42769  7rexfrabdioph  42770  jm2.27dlem1  42980  fnwe2lem2  43022  aomclem6  43030  deg1mhm  43171  hausgraph  43176  radcnvrat  44286  wessf1ornlem  45157  feqresmptf  45203  mccllem  45574  limcleqr  45621  limsupvaluz2  45715  supcnvlimsup  45717  limsupgtlem  45754  xlimconst2  45812  resincncf  45852  cncfperiod  45856  icccncfext  45864  cncfiooicclem1  45870  dvbdfbdioolem1  45905  dvnprodlem1  45923  dvnprodlem2  45924  itgioocnicc  45954  stoweidlem28  46005  fourierdlem18  46102  fourierdlem40  46124  fourierdlem42  46126  fourierdlem46  46129  fourierdlem51  46134  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem80  46163  fourierdlem81  46164  fourierdlem82  46165  fourierdlem84  46167  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem94  46177  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  sge0tsms  46357  sge0f1o  46359  sge0sup  46368  sge0less  46369  sge0ltfirp  46377  sge0resrnlem  46380  sge0resplit  46383  sge0le  46384  sge0split  46386  sge0fodjrnlem  46393  sge0iun  46396  meadjun  46439  meadjiunlem  46442  psmeasurelem  46447  caratheodory  46505  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  voncmpl  46598  mblvon  46616  smflimsuplem3  46799  afvres  47149  iccpartres  47380  iccelpart  47395  isubgredg  47827  isubgrgrim  47890  uhgrimisgrgric  47892  lincdifsn  48348  lindslinindimp2lem4  48385  lindslinindsimp2lem5  48386  lincresunit3lem2  48404  fdivmpt  48468  slotresfo  48821  basresposfo  48900  setrec2lem1  49505  setrecsres  49514  amgmwlem  49614