Theorem fvres 6851

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 3442	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5945	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6474	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6498	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6498	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2794	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   class class class wbr 5096   ↾ cres 5624  ℩cio 6444  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-res 5634  df-iota 6446  df-fv 6498

This theorem is referenced by:  fvresd  6852  funssfv  6853  fveqres  6876  feqresmpt  6901  dffv2  6927  eqfnun  6980  fvreseq0  6981  respreima  7009  fveqressseq  7022  ffvresb  7068  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  8052  fparlem2  8053  fsplitfpar  8058  fo2ndf  8061  f1o2ndf1  8062  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  8869  fofinf1o  9230  ixpfi2  9248  ttrclss  9627  updjudhcoinlf  9842  updjudhcoinrg  9843  updjud  9844  ackbij2lem2  10147  ackbij2lem3  10148  cfsmolem  10178  alephsing  10184  fpwwe2lem7  10546  inar1  10684  addpiord  10793  mulpiord  10794  fseq1p1m1  13512  injresinj  13705  seqfeq2  13946  seqres  13950  seqf1olem2  13963  hashgval  14254  hashinf  14256  hashgval2  14299  hashf1lem1  14376  pfxccat1  14623  shftidt  15003  climres  15496  fsumss  15646  isumclim3  15680  fsum2dlem  15691  ackbijnn  15749  fprodss  15869  fprod2dlem  15901  iprodclim3  15921  bpolylem  15969  fprodefsum  16016  reeff1  16043  bitsf1  16371  sadcadd  16383  sadadd2  16385  eucalgcvga  16511  eucalg  16512  unbenlem  16834  strfv2d  17126  setsid  17132  setsnid  17133  dfinito3  17927  dftermo3  17928  dmaf  17971  cdaf  17972  1stfcl  18118  2ndfcl  18119  resmgmhm  18634  resmhm  18743  resghm  19159  efgredlem  19674  gsumzaddlem  19848  dprdfadd  19949  dprdres  19957  dmdprdsplitlem  19966  dprdcntz2  19967  dmdprdsplit2lem  19974  dprdsplit  19977  dpjidcl  19987  ablfac1eu  20002  rngmgpf  20090  mgpf  20181  prdscrngd  20255  abvres  20762  reslmhm  21002  znf1o  21504  znunithash  21517  ltbwe  21997  subrgascl  22019  subrgasclcl  22020  smadiadetlem3  22610  lmres  23242  tx1cn  23551  tx2cn  23552  ptrescn  23581  cnmpt1st  23610  cnmpt2nd  23611  ptuncnv  23749  ptunhmeo  23750  cnextfres1  24010  prdstmdd  24066  prdsxmslem2  24471  subgnm2  24576  rescncf  24844  isncvsngp  25103  lmle  25255  ovoliunlem1  25457  ovolicc2lem4  25475  mblvol  25485  mbflimsup  25621  limcdif  25831  limcres  25841  dvres2lem  25865  dvlip  25952  dvlipcn  25953  dvlip2  25954  c1liplem1  25955  c1lip1  25956  c1lip3  25958  dvivthlem1  25967  lhop1lem  25972  lhop  25975  dvcvx  25979  ftc2ditglem  26006  itgsubstlem  26009  plyreres  26244  plyexmo  26275  aannenlem1  26290  taylthlem2  26336  taylthlem2OLD  26337  ulmres  26351  ulmss  26360  pserdvlem2  26392  reeff1o  26411  reefiso  26412  reefgim  26414  recosf1o  26498  resinf1o  26499  relogcl  26538  logef  26544  logeftb  26546  logltb  26563  logcn  26610  advlog  26617  advlogexp  26618  logtayl  26623  logccv  26626  dvcxp1  26703  dvcncxp1  26706  cxpcn  26708  cxpcnOLD  26709  loglesqrt  26725  dvatan  26899  leibpi  26906  efrlim  26933  efrlimOLD  26934  amgmlem  26954  lgamgulmlem2  26994  lgamcvg2  27019  wilthlem3  27034  ftalem3  27039  mpodvdsmulf1o  27158  fsumdvdsmul  27159  dvdsmulf1o  27160  fsumdvdsmulOLD  27161  dchrelbas2  27202  dchrabs  27225  dchrisumlem1  27454  logdivsum  27498  log2sumbnd  27509  ostth2  27602  ostth  27604  sltres  27628  nodense  27658  nolt02o  27661  nogt01o  27662  noetainflem4  27706  onsiso  28236  bdayn0sf1o  28328  vtxdginducedm1lem3  29564  redwlk  29693  pthdivtx  29749  pthdlem1  29788  ex-fpar  30486  sspnval  30761  hhssnv  31288  hhssmetdval  31301  foresf1o  32528  1stpreimas  32734  cos9thpiminply  33894  xpinpreima  34012  xpinpreima2  34013  cnre2csqlem  34016  zzsnm  34065  cnzh  34074  rezh  34075  measres  34328  cntmeas  34332  cntnevol  34334  1stmbfm  34366  2ndmbfm  34367  carsggect  34424  omsmeas  34429  eulerpartgbij  34478  eulerpartlemgvv  34482  eulerpartlemgs2  34486  iwrdsplit  34493  fibp1  34507  coinfliplem  34585  coinflipprob  34586  gsumnunsn  34647  plyrecld  34655  signstres  34681  ftc2re  34704  bnj1253  35122  bnj1280  35125  f1resveqaeq  35190  noinfepregs  35238  gblacfnacd  35245  subfacp1lem3  35325  subfacp1lem5  35327  erdszelem8  35341  txsconnlem  35383  cvmfolem  35422  cvmliftmolem1  35424  cvmliftlem6  35433  cvmliftlem7  35434  cvmliftlem9  35436  satfsucom  35497  satom  35499  satfvsucom  35500  satf0sucom  35516  mrsubff1  35657  msubff1  35699  dfrdg2  35936  funpartfv  36088  filnetlem4  36524  icoreunrn  37503  finixpnum  37745  poimirlem3  37763  poimirlem4  37764  poimirlem8  37768  poimirlem26  37786  poimirlem27  37787  itg2gt0cn  37815  areacirclem2  37849  areacirclem4  37851  sdclem2  37882  caures  37900  ismtyres  37948  diaintclN  41257  dibintclN  41366  dihintcl  41543  fsuppssindlem1  42776  imaiinfv  42877  mzpcompact2lem  42935  2rexfrabdioph  42980  3rexfrabdioph  42981  4rexfrabdioph  42982  6rexfrabdioph  42983  7rexfrabdioph  42984  jm2.27dlem1  43193  fnwe2lem2  43235  aomclem6  43243  deg1mhm  43384  hausgraph  43389  radcnvrat  44497  wessf1ornlem  45371  feqresmptf  45417  mccllem  45785  limcleqr  45830  limsupvaluz2  45924  supcnvlimsup  45926  limsupgtlem  45963  xlimconst2  46021  resincncf  46061  cncfperiod  46065  icccncfext  46073  cncfiooicclem1  46079  dvbdfbdioolem1  46114  dvnprodlem1  46132  dvnprodlem2  46133  itgioocnicc  46163  stoweidlem28  46214  fourierdlem18  46311  fourierdlem40  46333  fourierdlem42  46335  fourierdlem46  46338  fourierdlem51  46343  fourierdlem70  46362  fourierdlem71  46363  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem80  46372  fourierdlem81  46373  fourierdlem82  46374  fourierdlem84  46376  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem92  46384  fourierdlem93  46385  fourierdlem94  46386  fourierdlem101  46393  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  fourierdlem112  46404  fourierdlem113  46405  sge0tsms  46566  sge0f1o  46568  sge0sup  46577  sge0less  46578  sge0ltfirp  46586  sge0resrnlem  46589  sge0resplit  46592  sge0le  46593  sge0split  46595  sge0fodjrnlem  46602  sge0iun  46605  meadjun  46648  meadjiunlem  46651  psmeasurelem  46656  caratheodory  46714  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvlelem4  46784  voncmpl  46807  mblvon  46825  smflimsuplem3  47008  cjnpoly  47077  afvres  47360  iccpartres  47606  iccelpart  47621  isubgredg  48054  isubgrgrim  48117  uhgrimisgrgric  48119  lincdifsn  48612  lindslinindimp2lem4  48649  lindslinindsimp2lem5  48650  lincresunit3lem2  48668  fdivmpt  48728  slotresfo  49086  basresposfo  49165  oppff1  49335  setrec2lem1  49880  setrecsres  49889  amgmwlem  49989