Theorem fvres 6908

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 3479	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5989	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 537	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6525	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6549	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6549	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2798	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   class class class wbr 5148   ↾ cres 5678  ℩cio 6491  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-res 5688  df-iota 6493  df-fv 6549

This theorem is referenced by:  fvresd  6909  funssfv  6910  fveqres  6936  feqresmpt  6959  dffv2  6984  eqfnun  7036  fvreseq0  7037  respreima  7065  fveqressseq  7079  ffvresb  7121  fnressn  7153  fressnfv  7155  fvresi  7168  funfvima  7229  funiunfv  7244  soisores  7321  isores3  7329  isoini2  7333  fvresval  7352  ofres  7686  f1oweALT  7956  offres  7967  fo1stres  7998  fo2ndres  7999  fparlem1  8095  fparlem2  8096  fsplitfpar  8101  fo2ndf  8104  f1o2ndf1  8105  fnsuppres  8173  wfrlem4OLD  8309  tfrlem1  8373  fr0g  8433  frsuc  8434  tz7.48lem  8438  seqomlem1  8447  seqomlem2  8448  seqomlem3  8449  seqomlem4  8450  onasuc  8525  onmsuc  8526  onesuc  8527  resixp  8924  fofinf1o  9324  ixpfi2  9347  ttrclss  9712  updjudhcoinlf  9924  updjudhcoinrg  9925  updjud  9926  ackbij2lem2  10232  ackbij2lem3  10233  cfsmolem  10262  alephsing  10268  fpwwe2lem7  10629  inar1  10767  addpiord  10876  mulpiord  10877  fseq1p1m1  13572  injresinj  13750  seqfeq2  13988  seqres  13992  seqf1olem2  14005  hashgval  14290  hashinf  14292  hashgval2  14335  hashf1lem1  14412  hashf1lem1OLD  14413  pfxccat1  14649  shftidt  15026  climres  15516  fsumss  15668  isumclim3  15702  fsum2dlem  15713  ackbijnn  15771  fprodss  15889  fprod2dlem  15921  iprodclim3  15941  bpolylem  15989  fprodefsum  16035  reeff1  16060  bitsf1  16384  sadcadd  16396  sadadd2  16398  eucalgcvga  16520  eucalg  16521  unbenlem  16838  strfv2d  17132  setsid  17138  setsnid  17139  setsnidOLD  17140  dfinito3  17952  dftermo3  17953  dmaf  17996  cdaf  17997  1stfcl  18146  2ndfcl  18147  resmhm  18698  resghm  19103  efgredlem  19610  gsumzaddlem  19784  dprdfadd  19885  dprdres  19893  dmdprdsplitlem  19902  dprdcntz2  19903  dmdprdsplit2lem  19910  dprdsplit  19913  dpjidcl  19923  ablfac1eu  19938  mgpf  20065  prdscrngd  20129  abvres  20440  reslmhm  20656  znf1o  21099  znunithash  21112  ltbwe  21591  subrgascl  21619  subrgasclcl  21620  smadiadetlem3  22162  lmres  22796  tx1cn  23105  tx2cn  23106  ptrescn  23135  cnmpt1st  23164  cnmpt2nd  23165  ptuncnv  23303  ptunhmeo  23304  cnextfres1  23564  prdstmdd  23620  prdsxmslem2  24030  subgnm2  24135  rescncf  24405  isncvsngp  24658  lmle  24810  ovoliunlem1  25011  ovolicc2lem4  25029  mblvol  25039  mbflimsup  25175  limcdif  25385  limcres  25395  dvres2lem  25419  dvlip  25502  dvlipcn  25503  dvlip2  25504  c1liplem1  25505  c1lip1  25506  c1lip3  25508  dvivthlem1  25517  lhop1lem  25522  lhop  25525  dvcvx  25529  ftc2ditglem  25554  itgsubstlem  25557  plyreres  25788  plyexmo  25818  aannenlem1  25833  taylthlem2  25878  ulmres  25892  ulmss  25901  pserdvlem2  25932  reeff1o  25951  reefiso  25952  reefgim  25954  recosf1o  26036  resinf1o  26037  relogcl  26076  logef  26082  logeftb  26084  logltb  26100  logcn  26147  advlog  26154  advlogexp  26155  logtayl  26160  logccv  26163  dvcxp1  26238  dvcncxp1  26241  cxpcn  26243  loglesqrt  26256  dvatan  26430  leibpi  26437  efrlim  26464  amgmlem  26484  lgamgulmlem2  26524  lgamcvg2  26549  wilthlem3  26564  ftalem3  26569  dvdsmulf1o  26688  fsumdvdsmul  26689  dchrelbas2  26730  dchrabs  26753  dchrisumlem1  26982  logdivsum  27026  log2sumbnd  27037  ostth2  27130  ostth  27132  sltres  27155  nodense  27185  nolt02o  27188  nogt01o  27189  noetainflem4  27233  vtxdginducedm1lem3  28788  redwlk  28919  pthdivtx  28976  pthdlem1  29013  ex-fpar  29705  sspnval  29978  hhssnv  30505  hhssmetdval  30518  foresf1o  31730  1stpreimas  31915  xpinpreima  32875  xpinpreima2  32876  cnre2csqlem  32879  rmulccn  32897  zzsnm  32928  cnzh  32939  rezh  32940  measres  33209  cntmeas  33213  cntnevol  33215  1stmbfm  33248  2ndmbfm  33249  carsggect  33306  omsmeas  33311  eulerpartgbij  33360  eulerpartlemgvv  33364  eulerpartlemgs2  33368  iwrdsplit  33375  fibp1  33389  coinfliplem  33466  coinflipprob  33467  gsumnunsn  33541  plyrecld  33549  signstres  33575  ftc2re  33599  bnj1253  34017  bnj1280  34020  f1resveqaeq  34077  subfacp1lem3  34162  subfacp1lem5  34164  erdszelem8  34178  txsconnlem  34220  cvmfolem  34259  cvmliftmolem1  34261  cvmliftlem6  34270  cvmliftlem7  34271  cvmliftlem9  34273  satfsucom  34334  satom  34336  satfvsucom  34337  satf0sucom  34353  mrsubff1  34494  msubff1  34536  dfrdg2  34756  funpartfv  34906  gg-rmulccn  35168  gg-cxpcn  35173  filnetlem4  35255  icoreunrn  36229  finixpnum  36462  poimirlem3  36480  poimirlem4  36481  poimirlem8  36485  poimirlem26  36503  poimirlem27  36504  itg2gt0cn  36532  areacirclem2  36566  areacirclem4  36568  sdclem2  36599  caures  36617  ismtyres  36665  diaintclN  39918  dibintclN  40027  dihintcl  40204  fsuppssindlem1  41161  imaiinfv  41417  mzpcompact2lem  41475  2rexfrabdioph  41520  3rexfrabdioph  41521  4rexfrabdioph  41522  6rexfrabdioph  41523  7rexfrabdioph  41524  jm2.27dlem1  41734  fnwe2lem2  41779  aomclem6  41787  deg1mhm  41935  hausgraph  41940  radcnvrat  43059  wessf1ornlem  43868  feqresmptf  43917  mccllem  44300  limcleqr  44347  limsupvaluz2  44441  supcnvlimsup  44443  limsupgtlem  44480  xlimconst2  44538  resincncf  44578  cncfperiod  44582  icccncfext  44590  cncfiooicclem1  44596  dvbdfbdioolem1  44631  dvnprodlem1  44649  dvnprodlem2  44650  itgioocnicc  44680  stoweidlem28  44731  fourierdlem18  44828  fourierdlem40  44850  fourierdlem42  44852  fourierdlem46  44855  fourierdlem51  44860  fourierdlem70  44879  fourierdlem71  44880  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem78  44887  fourierdlem80  44889  fourierdlem81  44890  fourierdlem82  44891  fourierdlem84  44893  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem92  44901  fourierdlem93  44902  fourierdlem94  44903  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem112  44921  fourierdlem113  44922  sge0tsms  45083  sge0f1o  45085  sge0sup  45094  sge0less  45095  sge0ltfirp  45103  sge0resrnlem  45106  sge0resplit  45109  sge0le  45110  sge0split  45112  sge0fodjrnlem  45119  sge0iun  45122  meadjun  45165  meadjiunlem  45168  psmeasurelem  45173  caratheodory  45231  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvlelem4  45301  voncmpl  45324  mblvon  45342  smflimsuplem3  45525  afvres  45867  iccpartres  46073  iccelpart  46088  resmgmhm  46555  rngmgpf  46640  lincdifsn  47059  lindslinindimp2lem4  47096  lindslinindsimp2lem5  47097  lincresunit3lem2  47115  fdivmpt  47180  setrec2lem1  47692  setrecsres  47701  amgmwlem  47803