Theorem fvres 6904

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 3461	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5989	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 545	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6524	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6548	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6548	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2825	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   class class class wbr 5111   ↾ cres 5665  ℩cio 6494  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-res 5675  df-iota 6496  df-fv 6548

This theorem is used by:  fvresd  6905  funssfv  6906  fveqres  6929  feqresmpt  6954  dffv2  6980  eqfnun  7036  fvreseq0  7037  respreima  7065  fveqressseq  7078  ffvresb  7125  fnressn  7161  fressnfv  7163  fvresi  7177  funfvima  7235  funiunfv  7251  f1resveqaeq  7276  soisores  7334  isores3  7342  isoini2  7346  fvresval  7367  ofres  7703  f1oweALT  7975  offres  7986  fo1stres  8018  fo2ndres  8019  fparlem1  8113  fparlem2  8114  fsplitfpar  8119  fo2ndf  8122  f1o2ndf1  8123  fnsuppres  8193  tfrlem1  8368  fr0g  8429  frsuc  8430  tz7.48lem  8434  seqomlem1  8443  seqomlem2  8444  seqomlem3  8445  seqomlem4  8446  onasuc  8519  onmsuc  8520  onesuc  8521  resixp  8937  fofinf1o  9296  ixpfi2  9314  ttrclss  9696  updjudhcoinlf  9934  updjudhcoinrg  9935  updjud  9936  ackbij2lem2  10238  ackbij2lem3  10239  cfsmolem  10269  alephsing  10275  fpwwe2lem7  10637  inar1  10775  addpiord  10884  mulpiord  10885  fseq1p1m1  13643  injresinj  13837  seqfeq2  14079  seqres  14083  seqf1olem2  14096  hashgval  14387  hashinf  14389  hashgval2  14432  hashf1lem1  14510  pfxccat1  14761  shftidt  15143  climres  15650  fsumss  15799  isumclim3  15833  fsum2dlem  15844  ackbijnn  15905  fprodss  16025  fprod2dlem  16057  iprodclim3  16077  bpolylem  16124  fprodefsum  16171  reeff1  16198  bitsf1  16526  sadcadd  16538  sadadd2  16540  eucalgcvga  16666  eucalg  16667  unbenlem  16990  strfv2d  17283  setsid  17289  setsnid  17290  dfinito3  18084  dftermo3  18085  dmaf  18128  cdaf  18129  1stfcl  18275  2ndfcl  18276  resmgmhm  18801  resmhm  18916  resghm  19346  efgredlem  19861  gsumzaddlem  20035  dprdfadd  20136  dprdres  20144  dmdprdsplitlem  20153  dprdcntz2  20154  dmdprdsplit2lem  20161  dprdsplit  20164  dpjidcl  20174  ablfac1eu  20189  rngmgpf  20279  mgpf  20374  prdscrngd  20449  abvres  20984  reslmhm  21223  znf1o  21751  znunithash  21764  ltbwe  22245  subrgascl  22267  subrgasclcl  22268  smadiadetlem3  22875  lmres  23507  tx1cn  23817  tx2cn  23818  ptrescn  23847  cnmpt1st  23876  cnmpt2nd  23877  ptuncnv  24015  ptunhmeo  24016  cnextfres1  24276  prdstmdd  24332  prdsxmslem2  24737  subgnm2  24842  rescncf  25107  isncvsngp  25359  lmle  25511  ovoliunlem1  25712  ovolicc2lem4  25730  mblvol  25740  mbflimsup  25876  limcdif  26086  limcres  26096  dvres2lem  26120  dvlip  26203  dvlipcn  26204  dvlip2  26205  c1liplem1  26206  c1lip1  26207  c1lip3  26209  dvivthlem1  26218  lhop1lem  26223  lhop  26226  dvcvx  26230  ftc2ditglem  26255  itgsubstlem  26258  plyreres  26495  plyexmo  26525  aannenlem1  26542  taylthlem2  26588  ulmres  26602  ulmss  26611  pserdvlem2  26642  reeff1o  26661  reefiso  26662  reefgim  26664  recosf1o  26751  resinf1o  26752  relogcl  26791  logef  26797  logeftb  26799  logltb  26816  logcn  26863  advlog  26870  advlogexp  26871  logtayl  26876  logccv  26879  dvcxp1  26956  dvcncxp1  26959  cxpcn  26961  loglesqrt  26977  dvatan  27151  leibpi  27158  efrlim  27185  amgmlem  27205  lgamgulmlem2  27245  lgamcvg2  27270  wilthlem3  27285  ftalem3  27290  mpodvdsmulf1o  27409  fsumdvdsmul  27410  dvdsmulf1o  27411  dchrelbas2  27452  dchrabs  27475  dchrisumlem1  27704  logdivsum  27748  log2sumbnd  27759  ostth2  27852  ostth  27854  ltsres  27877  nodense  27907  nolt02o  27910  nogt01o  27911  noetainflem4  27955  oniso  28515  bdayn0sf1o  28614  vtxdginducedm1lem3  29949  redwlk  30078  pthdivtx  30139  pthdlem1  30179  ex-fpar  30884  sspnval  31160  hhssnv  31687  hhssmetdval  31700  foresf1o  32921  1stpreimas  33122  cos9thpiminply  34242  xpinpreima  34360  xpinpreima2  34361  cnre2csqlem  34364  zzsnm  34413  cnzh  34422  rezh  34423  measres  34677  cntmeas  34681  cntnevol  34683  1stmbfm  34715  2ndmbfm  34716  carsggect  34773  omsmeas  34778  eulerpartgbij  34827  eulerpartlemgvv  34831  eulerpartlemgs2  34835  iwrdsplit  34842  fibp1  34856  coinfliplem  34934  coinflipprob  34935  gsumnunsn  34996  plyrecld  35001  signstres  35027  ftc2re  35050  bnj1253  35470  bnj1280  35473  noinfepregs  35603  gblacfnacd  35643  subfacp1lem3  35711  subfacp1lem5  35713  erdszelem8  35727  txsconnlem  35769  cvmfolem  35808  cvmliftmolem1  35810  cvmliftlem6  35819  cvmliftlem7  35820  cvmliftlem9  35822  satfsucom  35883  satom  35885  satfvsucom  35886  satf0sucom  35902  mrsubff1  36043  msubff1  36085  dfrdg2  36322  funpartfv  36474  filnetlem4  36949  icoreunrn  38062  finixpnum  38313  poimirlem3  38331  poimirlem4  38332  poimirlem8  38336  poimirlem26  38354  poimirlem27  38355  itg2gt0cn  38383  areacirclem2  38417  areacirclem4  38419  sdclem2  38451  caures  38469  ismtyres  38517  diaintclN  41890  dibintclN  41999  dihintcl  42176  fsuppssindlem1  43381  imaiinfv  43482  mzpcompact2lem  43540  2rexfrabdioph  43581  3rexfrabdioph  43582  4rexfrabdioph  43583  6rexfrabdioph  43584  7rexfrabdioph  43585  jm2.27dlem1  43794  fnwe2lem2  43836  aomclem6  43844  deg1mhm  43985  hausgraph  43990  radcnvrat  45082  hashnna  45786  hashomiso  45792  wessf1ornlem  45961  feqresmptf  46004  mccllem  46371  limcleqr  46416  limsupvaluz2  46510  supcnvlimsup  46512  limsupgtlem  46549  xlimconst2  46607  resincncf  46647  cncfperiod  46651  icccncfext  46659  cncfiooicclem1  46665  dvbdfbdioolem1  46700  dvnprodlem1  46718  dvnprodlem2  46719  itgioocnicc  46749  stoweidlem28  46800  fourierdlem18  46897  fourierdlem40  46919  fourierdlem42  46921  fourierdlem46  46924  fourierdlem51  46929  fourierdlem70  46948  fourierdlem71  46949  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem78  46956  fourierdlem80  46958  fourierdlem81  46959  fourierdlem82  46960  fourierdlem84  46962  fourierdlem89  46967  fourierdlem90  46968  fourierdlem91  46969  fourierdlem92  46970  fourierdlem93  46971  fourierdlem94  46972  fourierdlem101  46979  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  fourierdlem112  46990  fourierdlem113  46991  sge0tsms  47152  sge0f1o  47154  sge0sup  47163  sge0less  47164  sge0ltfirp  47172  sge0resrnlem  47175  sge0resplit  47178  sge0le  47179  sge0split  47181  sge0fodjrnlem  47188  sge0iun  47191  meadjun  47234  meadjiunlem  47237  psmeasurelem  47242  caratheodory  47300  hoidmvlelem2  47368  hoidmvlelem3  47369  hoidmvlelem4  47370  voncmpl  47393  mblvon  47411  smflimsuplem3  47594  cjnpoly  47684  afvres  47967  iccpartres  48225  iccelpart  48240  isubgredg  48689  isubgrgrim  48752  uhgrimisgrgric  48754  lincdifsn  49261  lindslinindimp2lem4  49298  lindslinindsimp2lem5  49299  lincresunit3lem2  49317  fdivmpt  49377  slotresfo  49734  basresposfo  49813  oppff1  49983  setrec2lem1  50528  setrecsres  50537  amgmwlem  50707