Theorem fvres 6683

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 3497	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5856	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 538	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6333	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6357	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6357	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2881	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110   class class class wbr 5058   ↾ cres 5551  ℩cio 6306  ‘cfv 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-xp 5555  df-res 5561  df-iota 6308  df-fv 6357

This theorem is referenced by:  fvresd  6684  funssfv  6685  fveqres  6706  feqresmpt  6728  dffv2  6750  fvreseq0  6802  respreima  6830  fveqressseq  6841  ffvresb  6882  fnressn  6914  fressnfv  6916  fvresi  6929  funfvima  6986  funiunfv  7001  soisores  7074  isores3  7082  isoini2  7086  ofres  7419  f1oweALT  7667  offres  7678  fo1stres  7709  fo2ndres  7710  fparlem1  7801  fparlem2  7802  fsplitfpar  7808  fo2ndf  7811  f1o2ndf1  7812  fnsuppres  7851  wfrlem4  7952  tfrlem1  8006  fr0g  8065  frsuc  8066  tz7.48lem  8071  seqomlem1  8080  seqomlem2  8081  seqomlem3  8082  seqomlem4  8083  onasuc  8147  onmsuc  8148  onesuc  8149  resixp  8491  fofinf1o  8793  ixpfi2  8816  updjudhcoinlf  9355  updjudhcoinrg  9356  updjud  9357  ackbij2lem2  9656  ackbij2lem3  9657  cfsmolem  9686  alephsing  9692  fpwwe2lem8  10053  inar1  10191  addpiord  10300  mulpiord  10301  fseq1p1m1  12975  injresinj  13152  seqfeq2  13387  seqres  13391  seqf1olem2  13404  hashgval  13687  hashinf  13689  hashgval2  13733  hashf1lem1  13807  pfxccat1  14058  shftidt  14435  climres  14926  fsumss  15076  isumclim3  15108  fsum2dlem  15119  ackbijnn  15177  fprodss  15296  fprod2dlem  15328  iprodclim3  15348  bpolylem  15396  fprodefsum  15442  reeff1  15467  bitsf1  15789  sadcadd  15801  sadadd2  15803  eucalgcvga  15924  eucalg  15925  unbenlem  16238  strfv2d  16523  setsid  16532  setsnid  16533  dmaf  17303  cdaf  17304  1stfcl  17441  2ndfcl  17442  resmhm  17979  resghm  18368  efgredlem  18867  gsumzaddlem  19035  dprdfadd  19136  dprdres  19144  dmdprdsplitlem  19153  dprdcntz2  19154  dmdprdsplit2lem  19161  dprdsplit  19164  dpjidcl  19174  ablfac1eu  19189  mgpf  19303  prdscrngd  19357  abvres  19604  reslmhm  19818  ltbwe  20247  subrgascl  20272  subrgasclcl  20273  znf1o  20692  znunithash  20705  smadiadetlem3  21271  lmres  21902  tx1cn  22211  tx2cn  22212  ptrescn  22241  cnmpt1st  22270  cnmpt2nd  22271  ptuncnv  22409  ptunhmeo  22410  cnextfres1  22670  prdstmdd  22726  prdsxmslem2  23133  subgnm2  23237  rescncf  23499  isncvsngp  23747  lmle  23898  ovoliunlem1  24097  ovolicc2lem4  24115  mblvol  24125  mbflimsup  24261  limcdif  24468  limcres  24478  dvres2lem  24502  dvlip  24584  dvlipcn  24585  dvlip2  24586  c1liplem1  24587  c1lip1  24588  c1lip3  24590  dvivthlem1  24599  lhop1lem  24604  lhop  24607  dvcvx  24611  ftc2ditglem  24636  itgsubstlem  24639  plyreres  24866  plyexmo  24896  aannenlem1  24911  taylthlem2  24956  ulmres  24970  ulmss  24979  pserdvlem2  25010  reeff1o  25029  reefiso  25030  reefgim  25032  recosf1o  25113  resinf1o  25114  relogcl  25153  logef  25159  logeftb  25161  logltb  25177  logcn  25224  advlog  25231  advlogexp  25232  logtayl  25237  logccv  25240  dvcxp1  25315  dvcncxp1  25318  cxpcn  25320  loglesqrt  25333  dvatan  25507  leibpi  25514  efrlim  25541  amgmlem  25561  lgamgulmlem2  25601  lgamcvg2  25626  wilthlem3  25641  ftalem3  25646  dvdsmulf1o  25765  fsumdvdsmul  25766  dchrelbas2  25807  dchrabs  25830  dchrisumlem1  26059  logdivsum  26103  log2sumbnd  26114  ostth2  26207  ostth  26209  vtxdginducedm1lem3  27317  redwlk  27448  pthdivtx  27504  pthdlem1  27541  ex-fpar  28235  sspnval  28508  hhssnv  29035  hhssmetdval  29048  foresf1o  30259  1stpreimas  30435  xpinpreima  31144  xpinpreima2  31145  cnre2csqlem  31148  rmulccn  31166  zzsnm  31197  cnzh  31206  rezh  31207  measres  31476  cntmeas  31480  cntnevol  31482  1stmbfm  31513  2ndmbfm  31514  carsggect  31571  omsmeas  31576  eulerpartgbij  31625  eulerpartlemgvv  31629  eulerpartlemgs2  31633  iwrdsplit  31640  fibp1  31654  coinfliplem  31731  coinflipprob  31732  gsumnunsn  31806  plyrecld  31814  signstres  31840  ftc2re  31864  bnj1253  32284  bnj1280  32287  f1resveqaeq  32353  subfacp1lem3  32424  subfacp1lem5  32426  erdszelem8  32440  txsconnlem  32482  cvmfolem  32521  cvmliftmolem1  32523  cvmliftlem6  32532  cvmliftlem7  32533  cvmliftlem9  32535  satfsucom  32596  satom  32598  satfvsucom  32599  satf0sucom  32615  mrsubff1  32756  msubff1  32798  fvresval  33005  dfrdg2  33035  sltres  33164  nodense  33191  nolt02o  33194  funpartfv  33401  filnetlem4  33724  icoreunrn  34634  finixpnum  34871  poimirlem3  34889  poimirlem4  34890  poimirlem8  34894  poimirlem26  34912  poimirlem27  34913  itg2gt0cn  34941  areacirclem2  34977  areacirclem4  34979  eqfnun  34991  sdclem2  35011  caures  35029  ismtyres  35080  diaintclN  38188  dibintclN  38297  dihintcl  38474  imaiinfv  39283  mzpcompact2lem  39341  2rexfrabdioph  39386  3rexfrabdioph  39387  4rexfrabdioph  39388  6rexfrabdioph  39389  7rexfrabdioph  39390  jm2.27dlem1  39599  fnwe2lem2  39644  aomclem6  39652  deg1mhm  39800  hausgraph  39805  radcnvrat  40639  wessf1ornlem  41438  feqresmptf  41492  mccllem  41871  limcleqr  41918  limsupvaluz2  42012  supcnvlimsup  42014  limsupgtlem  42051  xlimconst2  42109  resincncf  42151  cncfperiod  42155  icccncfext  42163  cncfiooicclem1  42169  dvbdfbdioolem1  42206  dvnprodlem1  42224  dvnprodlem2  42225  itgioocnicc  42255  stoweidlem28  42307  fourierdlem18  42404  fourierdlem40  42426  fourierdlem42  42428  fourierdlem46  42431  fourierdlem51  42436  fourierdlem70  42455  fourierdlem71  42456  fourierdlem73  42458  fourierdlem74  42459  fourierdlem75  42460  fourierdlem76  42461  fourierdlem78  42463  fourierdlem80  42465  fourierdlem81  42466  fourierdlem82  42467  fourierdlem84  42469  fourierdlem89  42474  fourierdlem90  42475  fourierdlem91  42476  fourierdlem92  42477  fourierdlem93  42478  fourierdlem94  42479  fourierdlem101  42486  fourierdlem103  42488  fourierdlem104  42489  fourierdlem111  42496  fourierdlem112  42497  fourierdlem113  42498  sge0tsms  42656  sge0f1o  42658  sge0sup  42667  sge0less  42668  sge0ltfirp  42676  sge0resrnlem  42679  sge0resplit  42682  sge0le  42683  sge0split  42685  sge0fodjrnlem  42692  sge0iun  42695  meadjun  42738  meadjiunlem  42741  psmeasurelem  42746  caratheodory  42804  hoidmvlelem2  42872  hoidmvlelem3  42873  hoidmvlelem4  42874  voncmpl  42897  mblvon  42915  smflimsuplem3  43090  afvres  43365  iccpartres  43572  iccelpart  43587  resmgmhm  44059  lincdifsn  44473  lindslinindimp2lem4  44510  lindslinindsimp2lem5  44511  lincresunit3lem2  44529  fdivmpt  44594  setrec2lem1  44790  setrecsres  44798  amgmwlem  44897