Theorem fvres 6841

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 3440	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5939	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6466	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6490	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6490	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2789	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   class class class wbr 5092   ↾ cres 5621  ℩cio 6436  ‘cfv 6482

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-res 5631  df-iota 6438  df-fv 6490

This theorem is referenced by:  fvresd  6842  funssfv  6843  fveqres  6867  feqresmpt  6892  dffv2  6918  eqfnun  6971  fvreseq0  6972  respreima  7000  fveqressseq  7013  ffvresb  7059  fnressn  7092  fressnfv  7094  fvresi  7109  funfvima  7166  funiunfv  7184  soisores  7264  isores3  7272  isoini2  7276  fvresval  7295  ofres  7632  f1oweALT  7907  offres  7918  fo1stres  7950  fo2ndres  7951  fparlem1  8045  fparlem2  8046  fsplitfpar  8051  fo2ndf  8054  f1o2ndf1  8055  fnsuppres  8124  tfrlem1  8298  fr0g  8358  frsuc  8359  tz7.48lem  8363  seqomlem1  8372  seqomlem2  8373  seqomlem3  8374  seqomlem4  8375  onasuc  8446  onmsuc  8447  onesuc  8448  resixp  8860  fofinf1o  9222  ixpfi2  9240  ttrclss  9616  updjudhcoinlf  9828  updjudhcoinrg  9829  updjud  9830  ackbij2lem2  10133  ackbij2lem3  10134  cfsmolem  10164  alephsing  10170  fpwwe2lem7  10531  inar1  10669  addpiord  10778  mulpiord  10779  fseq1p1m1  13501  injresinj  13691  seqfeq2  13932  seqres  13936  seqf1olem2  13949  hashgval  14240  hashinf  14242  hashgval2  14285  hashf1lem1  14362  pfxccat1  14608  shftidt  14989  climres  15482  fsumss  15632  isumclim3  15666  fsum2dlem  15677  ackbijnn  15735  fprodss  15855  fprod2dlem  15887  iprodclim3  15907  bpolylem  15955  fprodefsum  16002  reeff1  16029  bitsf1  16357  sadcadd  16369  sadadd2  16371  eucalgcvga  16497  eucalg  16498  unbenlem  16820  strfv2d  17112  setsid  17118  setsnid  17119  dfinito3  17912  dftermo3  17913  dmaf  17956  cdaf  17957  1stfcl  18103  2ndfcl  18104  resmgmhm  18585  resmhm  18694  resghm  19111  efgredlem  19626  gsumzaddlem  19800  dprdfadd  19901  dprdres  19909  dmdprdsplitlem  19918  dprdcntz2  19919  dmdprdsplit2lem  19926  dprdsplit  19929  dpjidcl  19939  ablfac1eu  19954  rngmgpf  20042  mgpf  20133  prdscrngd  20207  abvres  20716  reslmhm  20956  znf1o  21458  znunithash  21471  ltbwe  21949  subrgascl  21971  subrgasclcl  21972  smadiadetlem3  22553  lmres  23185  tx1cn  23494  tx2cn  23495  ptrescn  23524  cnmpt1st  23553  cnmpt2nd  23554  ptuncnv  23692  ptunhmeo  23693  cnextfres1  23953  prdstmdd  24009  prdsxmslem2  24415  subgnm2  24520  rescncf  24788  isncvsngp  25047  lmle  25199  ovoliunlem1  25401  ovolicc2lem4  25419  mblvol  25429  mbflimsup  25565  limcdif  25775  limcres  25785  dvres2lem  25809  dvlip  25896  dvlipcn  25897  dvlip2  25898  c1liplem1  25899  c1lip1  25900  c1lip3  25902  dvivthlem1  25911  lhop1lem  25916  lhop  25919  dvcvx  25923  ftc2ditglem  25950  itgsubstlem  25953  plyreres  26188  plyexmo  26219  aannenlem1  26234  taylthlem2  26280  taylthlem2OLD  26281  ulmres  26295  ulmss  26304  pserdvlem2  26336  reeff1o  26355  reefiso  26356  reefgim  26358  recosf1o  26442  resinf1o  26443  relogcl  26482  logef  26488  logeftb  26490  logltb  26507  logcn  26554  advlog  26561  advlogexp  26562  logtayl  26567  logccv  26570  dvcxp1  26647  dvcncxp1  26650  cxpcn  26652  cxpcnOLD  26653  loglesqrt  26669  dvatan  26843  leibpi  26850  efrlim  26877  efrlimOLD  26878  amgmlem  26898  lgamgulmlem2  26938  lgamcvg2  26963  wilthlem3  26978  ftalem3  26983  mpodvdsmulf1o  27102  fsumdvdsmul  27103  dvdsmulf1o  27104  fsumdvdsmulOLD  27105  dchrelbas2  27146  dchrabs  27169  dchrisumlem1  27398  logdivsum  27442  log2sumbnd  27453  ostth2  27546  ostth  27548  sltres  27572  nodense  27602  nolt02o  27605  nogt01o  27606  noetainflem4  27650  onsiso  28174  bdayn0sf1o  28264  vtxdginducedm1lem3  29487  redwlk  29616  pthdivtx  29672  pthdlem1  29711  ex-fpar  30406  sspnval  30681  hhssnv  31208  hhssmetdval  31221  foresf1o  32448  1stpreimas  32648  cos9thpiminply  33755  xpinpreima  33873  xpinpreima2  33874  cnre2csqlem  33877  zzsnm  33926  cnzh  33935  rezh  33936  measres  34189  cntmeas  34193  cntnevol  34195  1stmbfm  34228  2ndmbfm  34229  carsggect  34286  omsmeas  34291  eulerpartgbij  34340  eulerpartlemgvv  34344  eulerpartlemgs2  34348  iwrdsplit  34355  fibp1  34369  coinfliplem  34447  coinflipprob  34448  gsumnunsn  34509  plyrecld  34517  signstres  34543  ftc2re  34566  bnj1253  34984  bnj1280  34987  f1resveqaeq  35052  gblacfnacd  35075  subfacp1lem3  35155  subfacp1lem5  35157  erdszelem8  35171  txsconnlem  35213  cvmfolem  35252  cvmliftmolem1  35254  cvmliftlem6  35263  cvmliftlem7  35264  cvmliftlem9  35266  satfsucom  35327  satom  35329  satfvsucom  35330  satf0sucom  35346  mrsubff1  35487  msubff1  35529  dfrdg2  35769  funpartfv  35919  filnetlem4  36355  icoreunrn  37333  finixpnum  37585  poimirlem3  37603  poimirlem4  37604  poimirlem8  37608  poimirlem26  37626  poimirlem27  37627  itg2gt0cn  37655  areacirclem2  37689  areacirclem4  37691  sdclem2  37722  caures  37740  ismtyres  37788  diaintclN  41037  dibintclN  41146  dihintcl  41323  fsuppssindlem1  42564  imaiinfv  42666  mzpcompact2lem  42724  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  jm2.27dlem1  42982  fnwe2lem2  43024  aomclem6  43032  deg1mhm  43173  hausgraph  43178  radcnvrat  44287  wessf1ornlem  45163  feqresmptf  45209  mccllem  45578  limcleqr  45625  limsupvaluz2  45719  supcnvlimsup  45721  limsupgtlem  45758  xlimconst2  45816  resincncf  45856  cncfperiod  45860  icccncfext  45868  cncfiooicclem1  45874  dvbdfbdioolem1  45909  dvnprodlem1  45927  dvnprodlem2  45928  itgioocnicc  45958  stoweidlem28  46009  fourierdlem18  46106  fourierdlem40  46128  fourierdlem42  46130  fourierdlem46  46133  fourierdlem51  46138  fourierdlem70  46157  fourierdlem71  46158  fourierdlem73  46160  fourierdlem74  46161  fourierdlem75  46162  fourierdlem76  46163  fourierdlem78  46165  fourierdlem80  46167  fourierdlem81  46168  fourierdlem82  46169  fourierdlem84  46171  fourierdlem89  46176  fourierdlem90  46177  fourierdlem91  46178  fourierdlem92  46179  fourierdlem93  46180  fourierdlem94  46181  fourierdlem101  46188  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  fourierdlem112  46199  fourierdlem113  46200  sge0tsms  46361  sge0f1o  46363  sge0sup  46372  sge0less  46373  sge0ltfirp  46381  sge0resrnlem  46384  sge0resplit  46387  sge0le  46388  sge0split  46390  sge0fodjrnlem  46397  sge0iun  46400  meadjun  46443  meadjiunlem  46446  psmeasurelem  46451  caratheodory  46509  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem4  46579  voncmpl  46602  mblvon  46620  smflimsuplem3  46803  cjnpoly  46873  afvres  47156  iccpartres  47402  iccelpart  47417  isubgredg  47850  isubgrgrim  47913  uhgrimisgrgric  47915  lincdifsn  48409  lindslinindimp2lem4  48446  lindslinindsimp2lem5  48447  lincresunit3lem2  48465  fdivmpt  48525  slotresfo  48883  basresposfo  48962  oppff1  49133  setrec2lem1  49678  setrecsres  49687  amgmwlem  49787