Theorem fvres 6935

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 3458	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5995	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 545	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6549	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6574	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6574	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2823	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   class class class wbr 5108   ↾ cres 5660  ℩cio 6518  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-res 5670  df-iota 6520  df-fv 6574

This theorem is used by:  fvresd  6936  funssfv  6937  fveqres  6960  feqresmpt  6985  dffv2  7011  eqfnun  7067  fvreseq0  7068  respreima  7097  fveqressseq  7111  ffvresb  7158  fnressn  7194  fressnfv  7196  fvresi  7209  funfvima  7267  funiunfv  7283  f1resveqaeq  7308  soisores  7366  isores3  7374  isoini2  7378  fvresval  7399  ofres  7744  f1oweALT  8018  offres  8029  fo1stres  8061  fo2ndres  8062  fparlem1  8160  fparlem2  8161  fsplitfpar  8166  fo2ndf  8169  f1o2ndf1  8170  fnwe2lem3  8184  fnsuppres  8246  tfrlem1  8421  fr0g  8482  frsuc  8483  tz7.48lem  8488  tz7.48lemOLD  8489  seqomlem1  8498  seqomlem2  8499  seqomlem3  8500  seqomlem4  8501  onasuc  8574  onmsuc  8575  onesuc  8576  resixp  8999  fofinf1o  9359  ixpfi2  9377  ttrclss  9758  setrec2lem1  10011  updjudhcoinlf  10050  updjudhcoinrg  10051  updjud  10052  ackbij2lem2  10356  ackbij2lem3  10357  cfsmolem  10387  alephsing  10393  fpwwe2lem7  10761  inar1  10899  addpiord  11008  mulpiord  11009  fseq1p1m1  13772  injresinj  13966  seqfeq2  14208  seqres  14212  seqf1olem2  14225  hashgval  14518  hashinf  14520  hashgval2  14563  hashf1lem1  14641  pfxccat1  14893  shftidt  15278  climres  15786  fsumss  15935  isumclim3  15969  fsum2dlem  15980  ackbijnn  16041  fprodss  16159  fprod2dlem  16191  iprodclim3  16211  bpolylem  16258  fprodefsum  16305  reeff1  16332  bitsf1  16660  sadcadd  16672  sadadd2  16674  eucalgcvga  16805  eucalg  16806  unbenlem  17130  strfv2d  17423  setsid  17429  setsnid  17430  dfinito3  18230  dftermo3  18231  dmaf  18274  cdaf  18275  1stfcl  18421  2ndfcl  18422  resmgmhm  18950  resmhm  19066  resghm  19496  efgredlem  20012  gsumzaddlem  20186  dprdfadd  20287  dprdres  20295  dmdprdsplitlem  20304  dprdcntz2  20305  dmdprdsplit2lem  20312  dprdsplit  20315  dpjidcl  20325  ablfac1eu  20340  rngmgpf  20430  mgpf  20526  prdscrngd  20602  abvres  21139  reslmhm  21378  znf1o  21912  znunithash  21925  ltbwe  22408  subrgascl  22430  subrgasclcl  22431  smadiadetlem3  23038  lmres  23673  tx1cn  23983  tx2cn  23984  ptrescn  24013  cnmpt1st  24042  cnmpt2nd  24043  ptuncnv  24181  ptunhmeo  24182  cnextfres1  24442  prdstmdd  24498  prdsxmslem2  24903  subgnm2  25008  rescncf  25273  isncvsngp  25525  lmle  25677  ovoliunlem1  25878  ovolicc2lem4  25896  mblvol  25906  mbflimsup  26042  limcdif  26251  limcres  26261  dvres2lem  26285  dvlip  26368  dvlipcn  26369  dvlip2  26370  c1liplem1  26371  c1lip1  26372  c1lip3  26374  dvivthlem1  26383  lhop1lem  26388  lhop  26391  dvcvx  26395  ftc2ditglem  26420  itgsubstlem  26423  plyreres  26659  plyexmo  26691  aannenlem1  26712  taylthlem2  26758  ulmres  26772  ulmss  26781  pserdvlem2  26812  reeff1o  26831  reefiso  26832  reefgim  26834  recosf1o  26920  resinf1o  26921  relogcl  26960  logef  26966  logeftb  26968  logltb  26985  logcn  27032  advlog  27039  advlogexp  27040  logtayl  27045  logccv  27048  dvcxp1  27125  dvcncxp1  27128  cxpcn  27130  loglesqrt  27146  dvatan  27320  leibpi  27327  efrlim  27354  amgmlem  27374  lgamgulmlem2  27414  lgamcvg2  27439  wilthlem3  27454  ftalem3  27459  mpodvdsmulf1o  27578  fsumdvdsmul  27579  dvdsmulf1o  27580  dchrelbas2  27621  dchrabs  27644  dchrisumlem1  27873  logdivsum  27917  log2sumbnd  27928  ostth2  28021  ostth  28023  ltsres  28076  nodense  28106  nolt02o  28109  nogt01o  28110  noetainflem4  28154  oniso  28714  bdayn0sf1o  28813  vtxdginducedm1lem3  30179  redwlk  30308  pthdivtx  30369  pthdlem1  30409  ex-fpar  31120  sspnval  31396  hhssnv  31923  hhssmetdval  31936  foresf1o  33199  1stpreimas  33396  cos9thpiminply  34531  xpinpreima  34649  xpinpreima2  34650  cnre2csqlem  34653  zzsnm  34702  cnzh  34711  rezh  34712  measres  34966  cntmeas  34970  cntnevol  34972  1stmbfm  35003  2ndmbfm  35004  carsggect  35061  omsmeas  35066  eulerpartgbij  35115  eulerpartlemgvv  35119  eulerpartlemgs2  35123  iwrdsplit  35130  fibp1  35144  coinfliplem  35222  coinflipprob  35223  gsumnunsn  35284  plyrecld  35289  signstres  35315  ftc2re  35338  bnj1253  35758  bnj1280  35761  fwfffunres  35829  noinfepregs  35942  gblacfnacd  36070  subfacp1lem3  36155  subfacp1lem5  36157  erdszelem8  36171  txsconnlem  36213  cvmfolem  36252  cvmliftmolem1  36254  cvmliftlem6  36263  cvmliftlem7  36264  cvmliftlem9  36266  satfsucom  36327  satom  36329  satfvsucom  36330  satf0sucom  36346  mrsubff1  36487  msubff1  36529  dfrdg2  36772  funpartfv  36924  filnetlem4  37384  icoreunrn  38550  finixpnum  38796  poimirlem3  38809  poimirlem4  38810  poimirlem8  38814  poimirlem26  38832  poimirlem27  38833  itg2gt0cn  38861  areacirclem2  38895  areacirclem4  38897  sdclem2  38942  caures  38960  ismtyres  39008  diaintclN  42381  dibintclN  42490  dihintcl  42667  fsuppssindlem1  43885  imaiinfv  43970  mzpcompact2lem  44028  2rexfrabdioph  44069  3rexfrabdioph  44070  4rexfrabdioph  44071  6rexfrabdioph  44072  7rexfrabdioph  44073  jm2.27dlem1  44282  aomclem6  44327  deg1mhm  44463  hausgraph  44468  radcnvrat  45559  hashnna  46273  hashomiso  46279  wessf1ornlem  46473  feqresmptf  46516  mccllem  46882  limcleqr  46927  limsupvaluz2  47021  supcnvlimsup  47023  limsupgtlem  47060  xlimconst2  47118  resincncf  47158  cncfperiod  47162  icccncfext  47170  cncfiooicclem1  47176  dvbdfbdioolem1  47211  dvnprodlem1  47229  dvnprodlem2  47230  itgioocnicc  47260  stoweidlem28  47311  fourierdlem18  47408  fourierdlem40  47430  fourierdlem42  47432  fourierdlem46  47435  fourierdlem51  47440  fourierdlem70  47459  fourierdlem71  47460  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem78  47467  fourierdlem80  47469  fourierdlem81  47470  fourierdlem82  47471  fourierdlem84  47473  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem92  47481  fourierdlem93  47482  fourierdlem94  47483  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fourierdlem112  47501  fourierdlem113  47502  sge0tsms  47663  sge0f1o  47665  sge0sup  47674  sge0less  47675  sge0ltfirp  47683  sge0resrnlem  47686  sge0resplit  47689  sge0le  47690  sge0split  47692  sge0fodjrnlem  47699  sge0iun  47702  meadjun  47745  meadjiunlem  47748  psmeasurelem  47753  caratheodory  47811  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem4  47881  voncmpl  47904  mblvon  47922  smflimsuplem3  48105  cjnpoly  48212  sqrtrrnpoly  48215  afvres  48515  iccpartres  48773  iccelpart  48788  isubgredg  49237  isubgrgrim  49300  uhgrimisgrgric  49302  lincdifsn  49867  lindslinindimp2lem4  49904  lindslinindsimp2lem5  49905  lincresunit3lem2  49923  fdivmpt  49983  slotresfo  50344  basresposfo  50423  oppff1  50595  setrecsres  51201  amgmwlem  51415