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 5936	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6465	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6489	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6489	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2791	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   class class class wbr 5089   ↾ cres 5616  ℩cio 6435  ‘cfv 6481

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-xp 5620  df-res 5626  df-iota 6437  df-fv 6489

This theorem is referenced by:  fvresd  6842  funssfv  6843  fveqres  6866  feqresmpt  6891  dffv2  6917  eqfnun  6970  fvreseq0  6971  respreima  6999  fveqressseq  7012  ffvresb  7058  fnressn  7091  fressnfv  7093  fvresi  7107  funfvima  7164  funiunfv  7182  soisores  7261  isores3  7269  isoini2  7273  fvresval  7292  ofres  7629  f1oweALT  7904  offres  7915  fo1stres  7947  fo2ndres  7948  fparlem1  8042  fparlem2  8043  fsplitfpar  8048  fo2ndf  8051  f1o2ndf1  8052  fnsuppres  8121  tfrlem1  8295  fr0g  8355  frsuc  8356  tz7.48lem  8360  seqomlem1  8369  seqomlem2  8370  seqomlem3  8371  seqomlem4  8372  onasuc  8443  onmsuc  8444  onesuc  8445  resixp  8857  fofinf1o  9216  ixpfi2  9234  ttrclss  9610  updjudhcoinlf  9825  updjudhcoinrg  9826  updjud  9827  ackbij2lem2  10130  ackbij2lem3  10131  cfsmolem  10161  alephsing  10167  fpwwe2lem7  10528  inar1  10666  addpiord  10775  mulpiord  10776  fseq1p1m1  13498  injresinj  13691  seqfeq2  13932  seqres  13936  seqf1olem2  13949  hashgval  14240  hashinf  14242  hashgval2  14285  hashf1lem1  14362  pfxccat1  14609  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  18619  resmhm  18728  resghm  19144  efgredlem  19659  gsumzaddlem  19833  dprdfadd  19934  dprdres  19942  dmdprdsplitlem  19951  dprdcntz2  19952  dmdprdsplit2lem  19959  dprdsplit  19962  dpjidcl  19972  ablfac1eu  19987  rngmgpf  20075  mgpf  20166  prdscrngd  20240  abvres  20746  reslmhm  20986  znf1o  21488  znunithash  21501  ltbwe  21979  subrgascl  22001  subrgasclcl  22002  smadiadetlem3  22583  lmres  23215  tx1cn  23524  tx2cn  23525  ptrescn  23554  cnmpt1st  23583  cnmpt2nd  23584  ptuncnv  23722  ptunhmeo  23723  cnextfres1  23983  prdstmdd  24039  prdsxmslem2  24444  subgnm2  24549  rescncf  24817  isncvsngp  25076  lmle  25228  ovoliunlem1  25430  ovolicc2lem4  25448  mblvol  25458  mbflimsup  25594  limcdif  25804  limcres  25814  dvres2lem  25838  dvlip  25925  dvlipcn  25926  dvlip2  25927  c1liplem1  25928  c1lip1  25929  c1lip3  25931  dvivthlem1  25940  lhop1lem  25945  lhop  25948  dvcvx  25952  ftc2ditglem  25979  itgsubstlem  25982  plyreres  26217  plyexmo  26248  aannenlem1  26263  taylthlem2  26309  taylthlem2OLD  26310  ulmres  26324  ulmss  26333  pserdvlem2  26365  reeff1o  26384  reefiso  26385  reefgim  26387  recosf1o  26471  resinf1o  26472  relogcl  26511  logef  26517  logeftb  26519  logltb  26536  logcn  26583  advlog  26590  advlogexp  26591  logtayl  26596  logccv  26599  dvcxp1  26676  dvcncxp1  26679  cxpcn  26681  cxpcnOLD  26682  loglesqrt  26698  dvatan  26872  leibpi  26879  efrlim  26906  efrlimOLD  26907  amgmlem  26927  lgamgulmlem2  26967  lgamcvg2  26992  wilthlem3  27007  ftalem3  27012  mpodvdsmulf1o  27131  fsumdvdsmul  27132  dvdsmulf1o  27133  fsumdvdsmulOLD  27134  dchrelbas2  27175  dchrabs  27198  dchrisumlem1  27427  logdivsum  27471  log2sumbnd  27482  ostth2  27575  ostth  27577  sltres  27601  nodense  27631  nolt02o  27634  nogt01o  27635  noetainflem4  27679  onsiso  28205  bdayn0sf1o  28295  vtxdginducedm1lem3  29520  redwlk  29649  pthdivtx  29705  pthdlem1  29744  ex-fpar  30442  sspnval  30717  hhssnv  31244  hhssmetdval  31257  foresf1o  32484  1stpreimas  32687  cos9thpiminply  33801  xpinpreima  33919  xpinpreima2  33920  cnre2csqlem  33923  zzsnm  33972  cnzh  33981  rezh  33982  measres  34235  cntmeas  34239  cntnevol  34241  1stmbfm  34273  2ndmbfm  34274  carsggect  34331  omsmeas  34336  eulerpartgbij  34385  eulerpartlemgvv  34389  eulerpartlemgs2  34393  iwrdsplit  34400  fibp1  34414  coinfliplem  34492  coinflipprob  34493  gsumnunsn  34554  plyrecld  34562  signstres  34588  ftc2re  34611  bnj1253  35029  bnj1280  35032  f1resveqaeq  35097  gblacfnacd  35146  subfacp1lem3  35226  subfacp1lem5  35228  erdszelem8  35242  txsconnlem  35284  cvmfolem  35323  cvmliftmolem1  35325  cvmliftlem6  35334  cvmliftlem7  35335  cvmliftlem9  35337  satfsucom  35398  satom  35400  satfvsucom  35401  satf0sucom  35417  mrsubff1  35558  msubff1  35600  dfrdg2  35837  funpartfv  35987  filnetlem4  36423  icoreunrn  37401  finixpnum  37653  poimirlem3  37671  poimirlem4  37672  poimirlem8  37676  poimirlem26  37694  poimirlem27  37695  itg2gt0cn  37723  areacirclem2  37757  areacirclem4  37759  sdclem2  37790  caures  37808  ismtyres  37856  diaintclN  41105  dibintclN  41214  dihintcl  41391  fsuppssindlem1  42632  imaiinfv  42734  mzpcompact2lem  42792  2rexfrabdioph  42837  3rexfrabdioph  42838  4rexfrabdioph  42839  6rexfrabdioph  42840  7rexfrabdioph  42841  jm2.27dlem1  43050  fnwe2lem2  43092  aomclem6  43100  deg1mhm  43241  hausgraph  43246  radcnvrat  44355  wessf1ornlem  45230  feqresmptf  45276  mccllem  45645  limcleqr  45690  limsupvaluz2  45784  supcnvlimsup  45786  limsupgtlem  45823  xlimconst2  45881  resincncf  45921  cncfperiod  45925  icccncfext  45933  cncfiooicclem1  45939  dvbdfbdioolem1  45974  dvnprodlem1  45992  dvnprodlem2  45993  itgioocnicc  46023  stoweidlem28  46074  fourierdlem18  46171  fourierdlem40  46193  fourierdlem42  46195  fourierdlem46  46198  fourierdlem51  46203  fourierdlem70  46222  fourierdlem71  46223  fourierdlem73  46225  fourierdlem74  46226  fourierdlem75  46227  fourierdlem76  46228  fourierdlem78  46230  fourierdlem80  46232  fourierdlem81  46233  fourierdlem82  46234  fourierdlem84  46236  fourierdlem89  46241  fourierdlem90  46242  fourierdlem91  46243  fourierdlem92  46244  fourierdlem93  46245  fourierdlem94  46246  fourierdlem101  46253  fourierdlem103  46255  fourierdlem104  46256  fourierdlem111  46263  fourierdlem112  46264  fourierdlem113  46265  sge0tsms  46426  sge0f1o  46428  sge0sup  46437  sge0less  46438  sge0ltfirp  46446  sge0resrnlem  46449  sge0resplit  46452  sge0le  46453  sge0split  46455  sge0fodjrnlem  46462  sge0iun  46465  meadjun  46508  meadjiunlem  46511  psmeasurelem  46516  caratheodory  46574  hoidmvlelem2  46642  hoidmvlelem3  46643  hoidmvlelem4  46644  voncmpl  46667  mblvon  46685  smflimsuplem3  46868  cjnpoly  46928  afvres  47211  iccpartres  47457  iccelpart  47472  isubgredg  47905  isubgrgrim  47968  uhgrimisgrgric  47970  lincdifsn  48464  lindslinindimp2lem4  48501  lindslinindsimp2lem5  48502  lincresunit3lem2  48520  fdivmpt  48580  slotresfo  48938  basresposfo  49017  oppff1  49188  setrec2lem1  49733  setrecsres  49742  amgmwlem  49842