Theorem fvres 6901

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   class class class wbr 5113   ↾ cres 5664  ℩cio 6491  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-res 5674  df-iota 6493  df-fv 6545

This theorem is referenced by:  fvresd  6902  funssfv  6903  fveqres  6926  feqresmpt  6951  dffv2  6977  eqfnun  7033  fvreseq0  7034  respreima  7062  fveqressseq  7075  ffvresb  7122  fnressn  7156  fressnfv  7158  fvresi  7172  funfvima  7229  funiunfv  7247  soisores  7326  isores3  7334  isoini2  7338  fvresval  7357  ofres  7694  f1oweALT  7968  offres  7979  fo1stres  8011  fo2ndres  8012  fparlem1  8106  fparlem2  8107  fsplitfpar  8112  fo2ndf  8115  f1o2ndf1  8116  fnsuppres  8186  tfrlem1  8361  fr0g  8422  frsuc  8423  tz7.48lem  8427  seqomlem1  8436  seqomlem2  8437  seqomlem3  8438  seqomlem4  8439  onasuc  8512  onmsuc  8513  onesuc  8514  resixp  8930  fofinf1o  9288  ixpfi2  9306  ttrclss  9688  updjudhcoinlf  9917  updjudhcoinrg  9918  updjud  9919  ackbij2lem2  10221  ackbij2lem3  10222  cfsmolem  10253  alephsing  10259  fpwwe2lem7  10621  inar1  10759  addpiord  10868  mulpiord  10869  fseq1p1m1  13625  injresinj  13819  seqfeq2  14060  seqres  14064  seqf1olem2  14077  hashgval  14368  hashinf  14370  hashgval2  14413  hashf1lem1  14491  pfxccat1  14738  shftidt  15118  climres  15625  fsumss  15775  isumclim3  15809  fsum2dlem  15820  ackbijnn  15881  fprodss  16001  fprod2dlem  16033  iprodclim3  16053  bpolylem  16101  fprodefsum  16148  reeff1  16175  bitsf1  16503  sadcadd  16515  sadadd2  16517  eucalgcvga  16643  eucalg  16644  unbenlem  16967  strfv2d  17260  setsid  17266  setsnid  17267  dfinito3  18061  dftermo3  18062  dmaf  18105  cdaf  18106  1stfcl  18252  2ndfcl  18253  resmgmhm  18768  resmhm  18878  resghm  19301  efgredlem  19816  gsumzaddlem  19990  dprdfadd  20091  dprdres  20099  dmdprdsplitlem  20108  dprdcntz2  20109  dmdprdsplit2lem  20116  dprdsplit  20119  dpjidcl  20129  ablfac1eu  20144  rngmgpf  20234  mgpf  20329  prdscrngd  20402  abvres  20911  reslmhm  21150  znf1o  21669  znunithash  21682  ltbwe  22163  subrgascl  22185  subrgasclcl  22186  smadiadetlem3  22793  lmres  23425  tx1cn  23734  tx2cn  23735  ptrescn  23764  cnmpt1st  23793  cnmpt2nd  23794  ptuncnv  23932  ptunhmeo  23933  cnextfres1  24193  prdstmdd  24249  prdsxmslem2  24654  subgnm2  24759  rescncf  25024  isncvsngp  25276  lmle  25428  ovoliunlem1  25629  ovolicc2lem4  25647  mblvol  25657  mbflimsup  25793  limcdif  26003  limcres  26013  dvres2lem  26037  dvlip  26120  dvlipcn  26121  dvlip2  26122  c1liplem1  26123  c1lip1  26124  c1lip3  26126  dvivthlem1  26135  lhop1lem  26140  lhop  26143  dvcvx  26147  ftc2ditglem  26172  itgsubstlem  26175  plyreres  26412  plyexmo  26442  aannenlem1  26457  taylthlem2  26502  ulmres  26516  ulmss  26525  pserdvlem2  26556  reeff1o  26575  reefiso  26576  reefgim  26578  recosf1o  26665  resinf1o  26666  relogcl  26705  logef  26711  logeftb  26713  logltb  26730  logcn  26777  advlog  26784  advlogexp  26785  logtayl  26790  logccv  26793  dvcxp1  26870  dvcncxp1  26873  cxpcn  26875  loglesqrt  26891  dvatan  27065  leibpi  27072  efrlim  27099  amgmlem  27119  lgamgulmlem2  27159  lgamcvg2  27184  wilthlem3  27199  ftalem3  27204  mpodvdsmulf1o  27323  fsumdvdsmul  27324  dvdsmulf1o  27325  dchrelbas2  27366  dchrabs  27389  dchrisumlem1  27618  logdivsum  27662  log2sumbnd  27673  ostth2  27766  ostth  27768  ltsres  27791  nodense  27821  nolt02o  27824  nogt01o  27825  noetainflem4  27869  oniso  28429  bdayn0sf1o  28528  vtxdginducedm1lem3  29831  redwlk  29960  pthdivtx  30016  pthdlem1  30055  ex-fpar  30753  sspnval  31029  hhssnv  31556  hhssmetdval  31569  foresf1o  32790  1stpreimas  32991  cos9thpiminply  34122  xpinpreima  34240  xpinpreima2  34241  cnre2csqlem  34244  zzsnm  34293  cnzh  34302  rezh  34303  measres  34556  cntmeas  34560  cntnevol  34562  1stmbfm  34594  2ndmbfm  34595  carsggect  34652  omsmeas  34657  eulerpartgbij  34706  eulerpartlemgvv  34710  eulerpartlemgs2  34714  iwrdsplit  34721  fibp1  34735  coinfliplem  34813  coinflipprob  34814  gsumnunsn  34875  plyrecld  34880  signstres  34906  ftc2re  34929  bnj1253  35349  bnj1280  35352  f1resveqaeq  35416  noinfepregs  35468  gblacfnacd  35484  subfacp1lem3  35572  subfacp1lem5  35574  erdszelem8  35588  txsconnlem  35630  cvmfolem  35669  cvmliftmolem1  35671  cvmliftlem6  35680  cvmliftlem7  35681  cvmliftlem9  35683  satfsucom  35744  satom  35746  satfvsucom  35747  satf0sucom  35763  mrsubff1  35904  msubff1  35946  dfrdg2  36183  funpartfv  36335  filnetlem4  36780  icoreunrn  37892  finixpnum  38143  poimirlem3  38161  poimirlem4  38162  poimirlem8  38166  poimirlem26  38184  poimirlem27  38185  itg2gt0cn  38213  areacirclem2  38247  areacirclem4  38249  sdclem2  38280  caures  38298  ismtyres  38346  diaintclN  41721  dibintclN  41830  dihintcl  42007  fsuppssindlem1  43214  imaiinfv  43315  mzpcompact2lem  43373  2rexfrabdioph  43414  3rexfrabdioph  43415  4rexfrabdioph  43416  6rexfrabdioph  43417  7rexfrabdioph  43418  jm2.27dlem1  43627  fnwe2lem2  43669  aomclem6  43677  deg1mhm  43818  hausgraph  43823  radcnvrat  44915  hashnna  45619  hashomiso  45625  wessf1ornlem  45794  feqresmptf  45837  mccllem  46204  limcleqr  46249  limsupvaluz2  46343  supcnvlimsup  46345  limsupgtlem  46382  xlimconst2  46440  resincncf  46480  cncfperiod  46484  icccncfext  46492  cncfiooicclem1  46498  dvbdfbdioolem1  46533  dvnprodlem1  46551  dvnprodlem2  46552  itgioocnicc  46582  stoweidlem28  46633  fourierdlem18  46730  fourierdlem40  46752  fourierdlem42  46754  fourierdlem46  46757  fourierdlem51  46762  fourierdlem70  46781  fourierdlem71  46782  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem78  46789  fourierdlem80  46791  fourierdlem81  46792  fourierdlem82  46793  fourierdlem84  46795  fourierdlem89  46800  fourierdlem90  46801  fourierdlem91  46802  fourierdlem92  46803  fourierdlem93  46804  fourierdlem94  46805  fourierdlem101  46812  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  fourierdlem112  46823  fourierdlem113  46824  sge0tsms  46985  sge0f1o  46987  sge0sup  46996  sge0less  46997  sge0ltfirp  47005  sge0resrnlem  47008  sge0resplit  47011  sge0le  47012  sge0split  47014  sge0fodjrnlem  47021  sge0iun  47024  meadjun  47067  meadjiunlem  47070  psmeasurelem  47075  caratheodory  47133  hoidmvlelem2  47201  hoidmvlelem3  47202  hoidmvlelem4  47203  voncmpl  47226  mblvon  47244  smflimsuplem3  47427  cjnpoly  47514  afvres  47797  iccpartres  48055  iccelpart  48070  isubgredg  48519  isubgrgrim  48582  uhgrimisgrgric  48584  lincdifsn  49088  lindslinindimp2lem4  49125  lindslinindsimp2lem5  49126  lincresunit3lem2  49144  fdivmpt  49204  slotresfo  49561  basresposfo  49640  oppff1  49810  setrec2lem1  50355  setrecsres  50364  amgmwlem  50475