Theorem fvres 6939

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 3492	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 6018	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6557	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6581	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6581	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2805	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   class class class wbr 5166   ↾ cres 5702  ℩cio 6523  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-res 5712  df-iota 6525  df-fv 6581

This theorem is referenced by:  fvresd  6940  funssfv  6941  fveqres  6967  feqresmpt  6991  dffv2  7017  eqfnun  7070  fvreseq0  7071  respreima  7099  fveqressseq  7113  ffvresb  7159  fnressn  7192  fressnfv  7194  fvresi  7207  funfvima  7267  funiunfv  7285  soisores  7363  isores3  7371  isoini2  7375  fvresval  7394  ofres  7733  f1oweALT  8013  offres  8024  fo1stres  8056  fo2ndres  8057  fparlem1  8153  fparlem2  8154  fsplitfpar  8159  fo2ndf  8162  f1o2ndf1  8163  fnsuppres  8232  wfrlem4OLD  8368  tfrlem1  8432  fr0g  8492  frsuc  8493  tz7.48lem  8497  seqomlem1  8506  seqomlem2  8507  seqomlem3  8508  seqomlem4  8509  onasuc  8584  onmsuc  8585  onesuc  8586  resixp  8991  fofinf1o  9400  ixpfi2  9420  ttrclss  9789  updjudhcoinlf  10001  updjudhcoinrg  10002  updjud  10003  ackbij2lem2  10308  ackbij2lem3  10309  cfsmolem  10339  alephsing  10345  fpwwe2lem7  10706  inar1  10844  addpiord  10953  mulpiord  10954  fseq1p1m1  13658  injresinj  13838  seqfeq2  14076  seqres  14080  seqf1olem2  14093  hashgval  14382  hashinf  14384  hashgval2  14427  hashf1lem1  14504  pfxccat1  14750  shftidt  15131  climres  15621  fsumss  15773  isumclim3  15807  fsum2dlem  15818  ackbijnn  15876  fprodss  15996  fprod2dlem  16028  iprodclim3  16048  bpolylem  16096  fprodefsum  16143  reeff1  16168  bitsf1  16492  sadcadd  16504  sadadd2  16506  eucalgcvga  16633  eucalg  16634  unbenlem  16955  strfv2d  17249  setsid  17255  setsnid  17256  setsnidOLD  17257  dfinito3  18072  dftermo3  18073  dmaf  18116  cdaf  18117  1stfcl  18266  2ndfcl  18267  resmgmhm  18749  resmhm  18855  resghm  19272  efgredlem  19789  gsumzaddlem  19963  dprdfadd  20064  dprdres  20072  dmdprdsplitlem  20081  dprdcntz2  20082  dmdprdsplit2lem  20089  dprdsplit  20092  dpjidcl  20102  ablfac1eu  20117  rngmgpf  20184  mgpf  20275  prdscrngd  20345  abvres  20854  reslmhm  21074  znf1o  21593  znunithash  21606  ltbwe  22085  subrgascl  22113  subrgasclcl  22114  smadiadetlem3  22695  lmres  23329  tx1cn  23638  tx2cn  23639  ptrescn  23668  cnmpt1st  23697  cnmpt2nd  23698  ptuncnv  23836  ptunhmeo  23837  cnextfres1  24097  prdstmdd  24153  prdsxmslem2  24563  subgnm2  24668  rescncf  24942  isncvsngp  25202  lmle  25354  ovoliunlem1  25556  ovolicc2lem4  25574  mblvol  25584  mbflimsup  25720  limcdif  25931  limcres  25941  dvres2lem  25965  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  c1lip1  26056  c1lip3  26058  dvivthlem1  26067  lhop1lem  26072  lhop  26075  dvcvx  26079  ftc2ditglem  26106  itgsubstlem  26109  plyreres  26342  plyexmo  26373  aannenlem1  26388  taylthlem2  26434  taylthlem2OLD  26435  ulmres  26449  ulmss  26458  pserdvlem2  26490  reeff1o  26509  reefiso  26510  reefgim  26512  recosf1o  26595  resinf1o  26596  relogcl  26635  logef  26641  logeftb  26643  logltb  26660  logcn  26707  advlog  26714  advlogexp  26715  logtayl  26720  logccv  26723  dvcxp1  26800  dvcncxp1  26803  cxpcn  26805  cxpcnOLD  26806  loglesqrt  26822  dvatan  26996  leibpi  27003  efrlim  27030  efrlimOLD  27031  amgmlem  27051  lgamgulmlem2  27091  lgamcvg2  27116  wilthlem3  27131  ftalem3  27136  mpodvdsmulf1o  27255  fsumdvdsmul  27256  dvdsmulf1o  27257  fsumdvdsmulOLD  27258  dchrelbas2  27299  dchrabs  27322  dchrisumlem1  27551  logdivsum  27595  log2sumbnd  27606  ostth2  27699  ostth  27701  sltres  27725  nodense  27755  nolt02o  27758  nogt01o  27759  noetainflem4  27803  vtxdginducedm1lem3  29577  redwlk  29708  pthdivtx  29765  pthdlem1  29802  ex-fpar  30494  sspnval  30769  hhssnv  31296  hhssmetdval  31309  foresf1o  32532  1stpreimas  32717  xpinpreima  33852  xpinpreima2  33853  cnre2csqlem  33856  zzsnm  33905  cnzh  33916  rezh  33917  measres  34186  cntmeas  34190  cntnevol  34192  1stmbfm  34225  2ndmbfm  34226  carsggect  34283  omsmeas  34288  eulerpartgbij  34337  eulerpartlemgvv  34341  eulerpartlemgs2  34345  iwrdsplit  34352  fibp1  34366  coinfliplem  34443  coinflipprob  34444  gsumnunsn  34518  plyrecld  34526  signstres  34552  ftc2re  34575  bnj1253  34993  bnj1280  34996  f1resveqaeq  35061  gblacfnacd  35075  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem8  35166  txsconnlem  35208  cvmfolem  35247  cvmliftmolem1  35249  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem9  35261  satfsucom  35322  satom  35324  satfvsucom  35325  satf0sucom  35341  mrsubff1  35482  msubff1  35524  dfrdg2  35759  funpartfv  35909  filnetlem4  36347  icoreunrn  37325  finixpnum  37565  poimirlem3  37583  poimirlem4  37584  poimirlem8  37588  poimirlem26  37606  poimirlem27  37607  itg2gt0cn  37635  areacirclem2  37669  areacirclem4  37671  sdclem2  37702  caures  37720  ismtyres  37768  diaintclN  41015  dibintclN  41124  dihintcl  41301  fsuppssindlem1  42546  imaiinfv  42649  mzpcompact2lem  42707  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  jm2.27dlem1  42966  fnwe2lem2  43008  aomclem6  43016  deg1mhm  43161  hausgraph  43166  radcnvrat  44283  wessf1ornlem  45092  feqresmptf  45138  mccllem  45518  limcleqr  45565  limsupvaluz2  45659  supcnvlimsup  45661  limsupgtlem  45698  xlimconst2  45756  resincncf  45796  cncfperiod  45800  icccncfext  45808  cncfiooicclem1  45814  dvbdfbdioolem1  45849  dvnprodlem1  45867  dvnprodlem2  45868  itgioocnicc  45898  stoweidlem28  45949  fourierdlem18  46046  fourierdlem40  46068  fourierdlem42  46070  fourierdlem46  46073  fourierdlem51  46078  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem80  46107  fourierdlem81  46108  fourierdlem82  46109  fourierdlem84  46111  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem94  46121  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  sge0tsms  46301  sge0f1o  46303  sge0sup  46312  sge0less  46313  sge0ltfirp  46321  sge0resrnlem  46324  sge0resplit  46327  sge0le  46328  sge0split  46330  sge0fodjrnlem  46337  sge0iun  46340  meadjun  46383  meadjiunlem  46386  psmeasurelem  46391  caratheodory  46449  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  voncmpl  46542  mblvon  46560  smflimsuplem3  46743  afvres  47087  iccpartres  47292  iccelpart  47307  isubgrgrim  47781  uhgrimisgrgric  47783  lincdifsn  48153  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  lincresunit3lem2  48209  fdivmpt  48274  setrec2lem1  48785  setrecsres  48794  amgmwlem  48896