Theorem fvres 6902

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 3455	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5979	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 545	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6521	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6545	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6545	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2821	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   class class class wbr 5103   ↾ cres 5653  ℩cio 6491  ‘cfv 6537

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-res 5663  df-iota 6493  df-fv 6545

This theorem is used by:  fvresd  6903  funssfv  6904  fveqres  6927  feqresmpt  6952  dffv2  6978  eqfnun  7034  fvreseq0  7035  respreima  7063  fveqressseq  7077  ffvresb  7124  fnressn  7160  fressnfv  7162  fvresi  7176  funfvima  7234  funiunfv  7250  f1resveqaeq  7275  soisores  7333  isores3  7341  isoini2  7345  fvresval  7366  ofres  7710  f1oweALT  7982  offres  7993  fo1stres  8025  fo2ndres  8026  fparlem1  8121  fparlem2  8122  fsplitfpar  8127  fo2ndf  8130  f1o2ndf1  8131  fnsuppres  8201  tfrlem1  8376  fr0g  8437  frsuc  8438  tz7.48lem  8443  tz7.48lemOLD  8444  seqomlem1  8453  seqomlem2  8454  seqomlem3  8455  seqomlem4  8456  onasuc  8529  onmsuc  8530  onesuc  8531  resixp  8954  fofinf1o  9314  ixpfi2  9332  ttrclss  9714  setrec2lem1  9967  updjudhcoinlf  10006  updjudhcoinrg  10007  updjud  10008  ackbij2lem2  10310  ackbij2lem3  10311  cfsmolem  10341  alephsing  10347  fpwwe2lem7  10715  inar1  10853  addpiord  10962  mulpiord  10963  fseq1p1m1  13725  injresinj  13919  seqfeq2  14161  seqres  14165  seqf1olem2  14178  hashgval  14470  hashinf  14472  hashgval2  14515  hashf1lem1  14593  pfxccat1  14844  shftidt  15228  climres  15735  fsumss  15884  isumclim3  15918  fsum2dlem  15929  ackbijnn  15990  fprodss  16108  fprod2dlem  16140  iprodclim3  16160  bpolylem  16207  fprodefsum  16254  reeff1  16281  bitsf1  16609  sadcadd  16621  sadadd2  16623  eucalgcvga  16754  eucalg  16755  unbenlem  17079  strfv2d  17372  setsid  17378  setsnid  17379  dfinito3  18173  dftermo3  18174  dmaf  18217  cdaf  18218  1stfcl  18364  2ndfcl  18365  resmgmhm  18893  resmhm  19009  resghm  19439  efgredlem  19954  gsumzaddlem  20128  dprdfadd  20229  dprdres  20237  dmdprdsplitlem  20246  dprdcntz2  20247  dmdprdsplit2lem  20254  dprdsplit  20257  dpjidcl  20267  ablfac1eu  20282  rngmgpf  20372  mgpf  20468  prdscrngd  20544  abvres  21081  reslmhm  21320  znf1o  21850  znunithash  21863  ltbwe  22346  subrgascl  22368  subrgasclcl  22369  smadiadetlem3  22976  lmres  23611  tx1cn  23921  tx2cn  23922  ptrescn  23951  cnmpt1st  23980  cnmpt2nd  23981  ptuncnv  24119  ptunhmeo  24120  cnextfres1  24380  prdstmdd  24436  prdsxmslem2  24841  subgnm2  24946  rescncf  25211  isncvsngp  25463  lmle  25615  ovoliunlem1  25816  ovolicc2lem4  25834  mblvol  25844  mbflimsup  25980  limcdif  26189  limcres  26199  dvres2lem  26223  dvlip  26306  dvlipcn  26307  dvlip2  26308  c1liplem1  26309  c1lip1  26310  c1lip3  26312  dvivthlem1  26321  lhop1lem  26326  lhop  26329  dvcvx  26333  ftc2ditglem  26358  itgsubstlem  26361  plyreres  26597  plyexmo  26629  aannenlem1  26648  taylthlem2  26694  ulmres  26708  ulmss  26717  pserdvlem2  26748  reeff1o  26767  reefiso  26768  reefgim  26770  recosf1o  26856  resinf1o  26857  relogcl  26896  logef  26902  logeftb  26904  logltb  26921  logcn  26968  advlog  26975  advlogexp  26976  logtayl  26981  logccv  26984  dvcxp1  27061  dvcncxp1  27064  cxpcn  27066  loglesqrt  27082  dvatan  27256  leibpi  27263  efrlim  27290  amgmlem  27310  lgamgulmlem2  27350  lgamcvg2  27375  wilthlem3  27390  ftalem3  27395  mpodvdsmulf1o  27514  fsumdvdsmul  27515  dvdsmulf1o  27516  dchrelbas2  27557  dchrabs  27580  dchrisumlem1  27809  logdivsum  27853  log2sumbnd  27864  ostth2  27957  ostth  27959  ltsres  28012  nodense  28042  nolt02o  28045  nogt01o  28046  noetainflem4  28090  oniso  28650  bdayn0sf1o  28749  vtxdginducedm1lem3  30115  redwlk  30244  pthdivtx  30305  pthdlem1  30345  ex-fpar  31056  sspnval  31332  hhssnv  31859  hhssmetdval  31872  foresf1o  33093  1stpreimas  33292  cos9thpiminply  34413  xpinpreima  34531  xpinpreima2  34532  cnre2csqlem  34535  zzsnm  34584  cnzh  34593  rezh  34594  measres  34848  cntmeas  34852  cntnevol  34854  1stmbfm  34885  2ndmbfm  34886  carsggect  34943  omsmeas  34948  eulerpartgbij  34997  eulerpartlemgvv  35001  eulerpartlemgs2  35005  iwrdsplit  35012  fibp1  35026  coinfliplem  35104  coinflipprob  35105  gsumnunsn  35166  plyrecld  35171  signstres  35197  ftc2re  35220  bnj1253  35640  bnj1280  35643  noinfepregs  35784  gblacfnacd  35864  subfacp1lem3  35926  subfacp1lem5  35928  erdszelem8  35942  txsconnlem  35984  cvmfolem  36023  cvmliftmolem1  36025  cvmliftlem6  36034  cvmliftlem7  36035  cvmliftlem9  36037  satfsucom  36098  satom  36100  satfvsucom  36101  satf0sucom  36117  mrsubff1  36258  msubff1  36300  dfrdg2  36537  funpartfv  36689  filnetlem4  37149  icoreunrn  38262  finixpnum  38508  poimirlem3  38521  poimirlem4  38522  poimirlem8  38526  poimirlem26  38544  poimirlem27  38545  itg2gt0cn  38573  areacirclem2  38607  areacirclem4  38609  sdclem2  38656  caures  38674  ismtyres  38722  diaintclN  42095  dibintclN  42204  dihintcl  42381  fsuppssindlem1  43599  imaiinfv  43683  mzpcompact2lem  43741  2rexfrabdioph  43782  3rexfrabdioph  43783  4rexfrabdioph  43784  6rexfrabdioph  43785  7rexfrabdioph  43786  jm2.27dlem1  43995  fnwe2lem2  44037  aomclem6  44045  deg1mhm  44186  hausgraph  44191  radcnvrat  45283  hashnna  45987  hashomiso  45993  wessf1ornlem  46169  feqresmptf  46212  mccllem  46578  limcleqr  46623  limsupvaluz2  46717  supcnvlimsup  46719  limsupgtlem  46756  xlimconst2  46814  resincncf  46854  cncfperiod  46858  icccncfext  46866  cncfiooicclem1  46872  dvbdfbdioolem1  46907  dvnprodlem1  46925  dvnprodlem2  46926  itgioocnicc  46956  stoweidlem28  47007  fourierdlem18  47104  fourierdlem40  47126  fourierdlem42  47128  fourierdlem46  47131  fourierdlem51  47136  fourierdlem70  47155  fourierdlem71  47156  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem78  47163  fourierdlem80  47165  fourierdlem81  47166  fourierdlem82  47167  fourierdlem84  47169  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem92  47177  fourierdlem93  47178  fourierdlem94  47179  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  fourierdlem113  47198  sge0tsms  47359  sge0f1o  47361  sge0sup  47370  sge0less  47371  sge0ltfirp  47379  sge0resrnlem  47382  sge0resplit  47385  sge0le  47386  sge0split  47388  sge0fodjrnlem  47395  sge0iun  47398  meadjun  47441  meadjiunlem  47444  psmeasurelem  47449  caratheodory  47507  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvlelem4  47577  voncmpl  47600  mblvon  47618  smflimsuplem3  47801  cjnpoly  47908  sqrtrrnpoly  47911  afvres  48211  iccpartres  48469  iccelpart  48484  isubgredg  48933  isubgrgrim  48996  uhgrimisgrgric  48998  lincdifsn  49505  lindslinindimp2lem4  49542  lindslinindsimp2lem5  49543  lincresunit3lem2  49561  fdivmpt  49621  slotresfo  49976  basresposfo  50055  oppff1  50225  setrecsres  50764  amgmwlem  50956