Theorem fvres 6861

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 3446	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5955	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6484	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6508	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6508	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2797	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   class class class wbr 5100   ↾ cres 5634  ℩cio 6454  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-res 5644  df-iota 6456  df-fv 6508

This theorem is referenced by:  fvresd  6862  funssfv  6863  fveqres  6886  feqresmpt  6911  dffv2  6937  eqfnun  6991  fvreseq0  6992  respreima  7020  fveqressseq  7033  ffvresb  7080  fnressn  7113  fressnfv  7115  fvresi  7129  funfvima  7186  funiunfv  7204  soisores  7283  isores3  7291  isoini2  7295  fvresval  7314  ofres  7651  f1oweALT  7926  offres  7937  fo1stres  7969  fo2ndres  7970  fparlem1  8064  fparlem2  8065  fsplitfpar  8070  fo2ndf  8073  f1o2ndf1  8074  fnsuppres  8143  tfrlem1  8317  fr0g  8377  frsuc  8378  tz7.48lem  8382  seqomlem1  8391  seqomlem2  8392  seqomlem3  8393  seqomlem4  8394  onasuc  8465  onmsuc  8466  onesuc  8467  resixp  8883  fofinf1o  9244  ixpfi2  9262  ttrclss  9641  updjudhcoinlf  9856  updjudhcoinrg  9857  updjud  9858  ackbij2lem2  10161  ackbij2lem3  10162  cfsmolem  10192  alephsing  10198  fpwwe2lem7  10560  inar1  10698  addpiord  10807  mulpiord  10808  fseq1p1m1  13526  injresinj  13719  seqfeq2  13960  seqres  13964  seqf1olem2  13977  hashgval  14268  hashinf  14270  hashgval2  14313  hashf1lem1  14390  pfxccat1  14637  shftidt  15017  climres  15510  fsumss  15660  isumclim3  15694  fsum2dlem  15705  ackbijnn  15763  fprodss  15883  fprod2dlem  15915  iprodclim3  15935  bpolylem  15983  fprodefsum  16030  reeff1  16057  bitsf1  16385  sadcadd  16397  sadadd2  16399  eucalgcvga  16525  eucalg  16526  unbenlem  16848  strfv2d  17140  setsid  17146  setsnid  17147  dfinito3  17941  dftermo3  17942  dmaf  17985  cdaf  17986  1stfcl  18132  2ndfcl  18133  resmgmhm  18648  resmhm  18757  resghm  19173  efgredlem  19688  gsumzaddlem  19862  dprdfadd  19963  dprdres  19971  dmdprdsplitlem  19980  dprdcntz2  19981  dmdprdsplit2lem  19988  dprdsplit  19991  dpjidcl  20001  ablfac1eu  20016  rngmgpf  20104  mgpf  20195  prdscrngd  20269  abvres  20776  reslmhm  21016  znf1o  21518  znunithash  21531  ltbwe  22011  subrgascl  22033  subrgasclcl  22034  smadiadetlem3  22624  lmres  23256  tx1cn  23565  tx2cn  23566  ptrescn  23595  cnmpt1st  23624  cnmpt2nd  23625  ptuncnv  23763  ptunhmeo  23764  cnextfres1  24024  prdstmdd  24080  prdsxmslem2  24485  subgnm2  24590  rescncf  24858  isncvsngp  25117  lmle  25269  ovoliunlem1  25471  ovolicc2lem4  25489  mblvol  25499  mbflimsup  25635  limcdif  25845  limcres  25855  dvres2lem  25879  dvlip  25966  dvlipcn  25967  dvlip2  25968  c1liplem1  25969  c1lip1  25970  c1lip3  25972  dvivthlem1  25981  lhop1lem  25986  lhop  25989  dvcvx  25993  ftc2ditglem  26020  itgsubstlem  26023  plyreres  26258  plyexmo  26289  aannenlem1  26304  taylthlem2  26350  taylthlem2OLD  26351  ulmres  26365  ulmss  26374  pserdvlem2  26406  reeff1o  26425  reefiso  26426  reefgim  26428  recosf1o  26512  resinf1o  26513  relogcl  26552  logef  26558  logeftb  26560  logltb  26577  logcn  26624  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvcncxp1  26720  cxpcn  26722  cxpcnOLD  26723  loglesqrt  26739  dvatan  26913  leibpi  26920  efrlim  26947  efrlimOLD  26948  amgmlem  26968  lgamgulmlem2  27008  lgamcvg2  27033  wilthlem3  27048  ftalem3  27053  mpodvdsmulf1o  27172  fsumdvdsmul  27173  dvdsmulf1o  27174  fsumdvdsmulOLD  27175  dchrelbas2  27216  dchrabs  27239  dchrisumlem1  27468  logdivsum  27512  log2sumbnd  27523  ostth2  27616  ostth  27618  ltsres  27642  nodense  27672  nolt02o  27675  nogt01o  27676  noetainflem4  27720  oniso  28279  bdayn0sf1o  28378  vtxdginducedm1lem3  29627  redwlk  29756  pthdivtx  29812  pthdlem1  29851  ex-fpar  30549  sspnval  30825  hhssnv  31352  hhssmetdval  31365  foresf1o  32591  1stpreimas  32796  cos9thpiminply  33966  xpinpreima  34084  xpinpreima2  34085  cnre2csqlem  34088  zzsnm  34137  cnzh  34146  rezh  34147  measres  34400  cntmeas  34404  cntnevol  34406  1stmbfm  34438  2ndmbfm  34439  carsggect  34496  omsmeas  34501  eulerpartgbij  34550  eulerpartlemgvv  34554  eulerpartlemgs2  34558  iwrdsplit  34565  fibp1  34579  coinfliplem  34657  coinflipprob  34658  gsumnunsn  34719  plyrecld  34727  signstres  34753  ftc2re  34776  bnj1253  35193  bnj1280  35196  f1resveqaeq  35262  noinfepregs  35311  gblacfnacd  35318  subfacp1lem3  35398  subfacp1lem5  35400  erdszelem8  35414  txsconnlem  35456  cvmfolem  35495  cvmliftmolem1  35497  cvmliftlem6  35506  cvmliftlem7  35507  cvmliftlem9  35509  satfsucom  35570  satom  35572  satfvsucom  35573  satf0sucom  35589  mrsubff1  35730  msubff1  35772  dfrdg2  36009  funpartfv  36161  filnetlem4  36597  icoreunrn  37614  finixpnum  37856  poimirlem3  37874  poimirlem4  37875  poimirlem8  37879  poimirlem26  37897  poimirlem27  37898  itg2gt0cn  37926  areacirclem2  37960  areacirclem4  37962  sdclem2  37993  caures  38011  ismtyres  38059  diaintclN  41434  dibintclN  41543  dihintcl  41720  fsuppssindlem1  42949  imaiinfv  43050  mzpcompact2lem  43108  2rexfrabdioph  43153  3rexfrabdioph  43154  4rexfrabdioph  43155  6rexfrabdioph  43156  7rexfrabdioph  43157  jm2.27dlem1  43366  fnwe2lem2  43408  aomclem6  43416  deg1mhm  43557  hausgraph  43562  radcnvrat  44670  wessf1ornlem  45544  feqresmptf  45589  mccllem  45957  limcleqr  46002  limsupvaluz2  46096  supcnvlimsup  46098  limsupgtlem  46135  xlimconst2  46193  resincncf  46233  cncfperiod  46237  icccncfext  46245  cncfiooicclem1  46251  dvbdfbdioolem1  46286  dvnprodlem1  46304  dvnprodlem2  46305  itgioocnicc  46335  stoweidlem28  46386  fourierdlem18  46483  fourierdlem40  46505  fourierdlem42  46507  fourierdlem46  46510  fourierdlem51  46515  fourierdlem70  46534  fourierdlem71  46535  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem78  46542  fourierdlem80  46544  fourierdlem81  46545  fourierdlem82  46546  fourierdlem84  46548  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem92  46556  fourierdlem93  46557  fourierdlem94  46558  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem112  46576  fourierdlem113  46577  sge0tsms  46738  sge0f1o  46740  sge0sup  46749  sge0less  46750  sge0ltfirp  46758  sge0resrnlem  46761  sge0resplit  46764  sge0le  46765  sge0split  46767  sge0fodjrnlem  46774  sge0iun  46777  meadjun  46820  meadjiunlem  46823  psmeasurelem  46828  caratheodory  46886  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  voncmpl  46979  mblvon  46997  smflimsuplem3  47180  cjnpoly  47249  afvres  47532  iccpartres  47778  iccelpart  47793  isubgredg  48226  isubgrgrim  48289  uhgrimisgrgric  48291  lincdifsn  48784  lindslinindimp2lem4  48821  lindslinindsimp2lem5  48822  lincresunit3lem2  48840  fdivmpt  48900  slotresfo  49258  basresposfo  49337  oppff1  49507  setrec2lem1  50052  setrecsres  50061  amgmwlem  50161