Theorem fvres 6846

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 3435	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5940	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 540	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6469	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6493	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6493	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2799	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   class class class wbr 5072   ↾ cres 5620  ℩cio 6439  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-res 5630  df-iota 6441  df-fv 6493

This theorem is referenced by:  fvresd  6847  funssfv  6848  fveqres  6871  feqresmpt  6896  dffv2  6922  eqfnun  6978  fvreseq0  6979  respreima  7007  fveqressseq  7020  ffvresb  7067  fnressn  7101  fressnfv  7103  fvresi  7117  funfvima  7174  funiunfv  7192  soisores  7271  isores3  7279  isoini2  7283  fvresval  7302  ofres  7639  f1oweALT  7914  offres  7925  fo1stres  7957  fo2ndres  7958  fparlem1  8051  fparlem2  8052  fsplitfpar  8057  fo2ndf  8060  f1o2ndf1  8061  fnsuppres  8131  tfrlem1  8305  fr0g  8365  frsuc  8366  tz7.48lem  8370  seqomlem1  8379  seqomlem2  8380  seqomlem3  8381  seqomlem4  8382  onasuc  8453  onmsuc  8454  onesuc  8455  resixp  8871  fofinf1o  9232  ixpfi2  9250  ttrclss  9632  updjudhcoinlf  9847  updjudhcoinrg  9848  updjud  9849  ackbij2lem2  10152  ackbij2lem3  10153  cfsmolem  10183  alephsing  10189  fpwwe2lem7  10551  inar1  10689  addpiord  10798  mulpiord  10799  fseq1p1m1  13543  injresinj  13737  seqfeq2  13978  seqres  13982  seqf1olem2  13995  hashgval  14286  hashinf  14288  hashgval2  14331  hashf1lem1  14408  pfxccat1  14655  shftidt  15035  climres  15528  fsumss  15678  isumclim3  15712  fsum2dlem  15723  ackbijnn  15784  fprodss  15904  fprod2dlem  15936  iprodclim3  15956  bpolylem  16004  fprodefsum  16051  reeff1  16078  bitsf1  16406  sadcadd  16418  sadadd2  16420  eucalgcvga  16546  eucalg  16547  unbenlem  16870  strfv2d  17162  setsid  17168  setsnid  17169  dfinito3  17963  dftermo3  17964  dmaf  18007  cdaf  18008  1stfcl  18154  2ndfcl  18155  resmgmhm  18670  resmhm  18779  resghm  19198  efgredlem  19713  gsumzaddlem  19887  dprdfadd  19988  dprdres  19996  dmdprdsplitlem  20005  dprdcntz2  20006  dmdprdsplit2lem  20013  dprdsplit  20016  dpjidcl  20026  ablfac1eu  20041  rngmgpf  20129  mgpf  20220  prdscrngd  20292  abvres  20803  reslmhm  21042  znf1o  21526  znunithash  21539  ltbwe  22020  subrgascl  22042  subrgasclcl  22043  smadiadetlem3  22651  lmres  23283  tx1cn  23592  tx2cn  23593  ptrescn  23622  cnmpt1st  23651  cnmpt2nd  23652  ptuncnv  23790  ptunhmeo  23791  cnextfres1  24051  prdstmdd  24107  prdsxmslem2  24512  subgnm2  24617  rescncf  24882  isncvsngp  25134  lmle  25286  ovoliunlem1  25487  ovolicc2lem4  25505  mblvol  25515  mbflimsup  25651  limcdif  25861  limcres  25871  dvres2lem  25895  dvlip  25978  dvlipcn  25979  dvlip2  25980  c1liplem1  25981  c1lip1  25982  c1lip3  25984  dvivthlem1  25993  lhop1lem  25998  lhop  26001  dvcvx  26005  ftc2ditglem  26030  itgsubstlem  26033  plyreres  26267  plyexmo  26297  aannenlem1  26312  taylthlem2  26357  ulmres  26371  ulmss  26380  pserdvlem2  26411  reeff1o  26430  reefiso  26431  reefgim  26433  recosf1o  26517  resinf1o  26518  relogcl  26557  logef  26563  logeftb  26565  logltb  26582  logcn  26629  advlog  26636  advlogexp  26637  logtayl  26642  logccv  26645  dvcxp1  26722  dvcncxp1  26725  cxpcn  26727  loglesqrt  26743  dvatan  26917  leibpi  26924  efrlim  26951  amgmlem  26971  lgamgulmlem2  27011  lgamcvg2  27036  wilthlem3  27051  ftalem3  27056  mpodvdsmulf1o  27175  fsumdvdsmul  27176  dvdsmulf1o  27177  dchrelbas2  27218  dchrabs  27241  dchrisumlem1  27470  logdivsum  27514  log2sumbnd  27525  ostth2  27618  ostth  27620  ltsres  27644  nodense  27674  nolt02o  27677  nogt01o  27678  noetainflem4  27722  oniso  28281  bdayn0sf1o  28380  vtxdginducedm1lem3  29628  redwlk  29757  pthdivtx  29813  pthdlem1  29852  ex-fpar  30550  sspnval  30826  hhssnv  31353  hhssmetdval  31366  foresf1o  32592  1stpreimas  32798  cos9thpiminply  33972  xpinpreima  34090  xpinpreima2  34091  cnre2csqlem  34094  zzsnm  34143  cnzh  34152  rezh  34153  measres  34406  cntmeas  34410  cntnevol  34412  1stmbfm  34444  2ndmbfm  34445  carsggect  34502  omsmeas  34507  eulerpartgbij  34556  eulerpartlemgvv  34560  eulerpartlemgs2  34564  iwrdsplit  34571  fibp1  34585  coinfliplem  34663  coinflipprob  34664  gsumnunsn  34725  plyrecld  34733  signstres  34759  ftc2re  34782  bnj1253  35199  bnj1280  35202  f1resveqaeq  35266  noinfepregs  35314  gblacfnacd  35330  subfacp1lem3  35410  subfacp1lem5  35412  erdszelem8  35426  txsconnlem  35468  cvmfolem  35507  cvmliftmolem1  35509  cvmliftlem6  35518  cvmliftlem7  35519  cvmliftlem9  35521  satfsucom  35582  satom  35584  satfvsucom  35585  satf0sucom  35601  mrsubff1  35742  msubff1  35784  dfrdg2  36021  funpartfv  36173  filnetlem4  36609  icoreunrn  37721  finixpnum  37972  poimirlem3  37990  poimirlem4  37991  poimirlem8  37995  poimirlem26  38013  poimirlem27  38014  itg2gt0cn  38042  areacirclem2  38076  areacirclem4  38078  sdclem2  38109  caures  38127  ismtyres  38175  diaintclN  41550  dibintclN  41659  dihintcl  41836  fsuppssindlem1  43041  imaiinfv  43142  mzpcompact2lem  43200  2rexfrabdioph  43241  3rexfrabdioph  43242  4rexfrabdioph  43243  6rexfrabdioph  43244  7rexfrabdioph  43245  jm2.27dlem1  43454  fnwe2lem2  43496  aomclem6  43504  deg1mhm  43645  hausgraph  43650  radcnvrat  44758  wessf1ornlem  45632  feqresmptf  45675  mccllem  46042  limcleqr  46087  limsupvaluz2  46181  supcnvlimsup  46183  limsupgtlem  46220  xlimconst2  46278  resincncf  46318  cncfperiod  46322  icccncfext  46330  cncfiooicclem1  46336  dvbdfbdioolem1  46371  dvnprodlem1  46389  dvnprodlem2  46390  itgioocnicc  46420  stoweidlem28  46471  fourierdlem18  46568  fourierdlem40  46590  fourierdlem42  46592  fourierdlem46  46595  fourierdlem51  46600  fourierdlem70  46619  fourierdlem71  46620  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem78  46627  fourierdlem80  46629  fourierdlem81  46630  fourierdlem82  46631  fourierdlem84  46633  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem92  46641  fourierdlem93  46642  fourierdlem94  46643  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  sge0tsms  46823  sge0f1o  46825  sge0sup  46834  sge0less  46835  sge0ltfirp  46843  sge0resrnlem  46846  sge0resplit  46849  sge0le  46850  sge0split  46852  sge0fodjrnlem  46859  sge0iun  46862  meadjun  46905  meadjiunlem  46908  psmeasurelem  46913  caratheodory  46971  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  voncmpl  47064  mblvon  47082  smflimsuplem3  47265  cjnpoly  47352  afvres  47635  iccpartres  47893  iccelpart  47908  isubgredg  48357  isubgrgrim  48420  uhgrimisgrgric  48422  lincdifsn  48915  lindslinindimp2lem4  48952  lindslinindsimp2lem5  48953  lincresunit3lem2  48971  fdivmpt  49031  slotresfo  49389  basresposfo  49468  oppff1  49638  setrec2lem1  50183  setrecsres  50192  amgmwlem  50292