Theorem fvres 6909

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 3454	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5980	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 545	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6526	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6551	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6551	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2820	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   class class class wbr 5102   ↾ cres 5653  ℩cio 6495  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5657  df-res 5663  df-iota 6497  df-fv 6551

This theorem is used by:  fvresd  6910  funssfv  6911  fveqres  6934  feqresmpt  6959  dffv2  6985  eqfnun  7041  fvreseq0  7042  respreima  7070  fveqressseq  7084  ffvresb  7131  fnressn  7167  fressnfv  7169  fvresi  7182  funfvima  7240  funiunfv  7256  f1resveqaeq  7281  soisores  7339  isores3  7347  isoini2  7351  fvresval  7372  ofres  7716  f1oweALT  7988  offres  7999  fo1stres  8031  fo2ndres  8032  fparlem1  8129  fparlem2  8130  fsplitfpar  8135  fo2ndf  8138  f1o2ndf1  8139  fnwe2lem3  8153  fnsuppres  8215  tfrlem1  8390  fr0g  8451  frsuc  8452  tz7.48lem  8457  tz7.48lemOLD  8458  seqomlem1  8467  seqomlem2  8468  seqomlem3  8469  seqomlem4  8470  onasuc  8543  onmsuc  8544  onesuc  8545  resixp  8968  fofinf1o  9328  ixpfi2  9346  ttrclss  9728  setrec2lem1  9981  updjudhcoinlf  10020  updjudhcoinrg  10021  updjud  10022  ackbij2lem2  10324  ackbij2lem3  10325  cfsmolem  10355  alephsing  10361  fpwwe2lem7  10729  inar1  10867  addpiord  10976  mulpiord  10977  fseq1p1m1  13739  injresinj  13933  seqfeq2  14175  seqres  14179  seqf1olem2  14192  hashgval  14484  hashinf  14486  hashgval2  14529  hashf1lem1  14607  pfxccat1  14859  shftidt  15244  climres  15751  fsumss  15900  isumclim3  15934  fsum2dlem  15945  ackbijnn  16006  fprodss  16124  fprod2dlem  16156  iprodclim3  16176  bpolylem  16223  fprodefsum  16270  reeff1  16297  bitsf1  16625  sadcadd  16637  sadadd2  16639  eucalgcvga  16770  eucalg  16771  unbenlem  17095  strfv2d  17388  setsid  17394  setsnid  17395  dfinito3  18189  dftermo3  18190  dmaf  18233  cdaf  18234  1stfcl  18380  2ndfcl  18381  resmgmhm  18909  resmhm  19025  resghm  19455  efgredlem  19970  gsumzaddlem  20144  dprdfadd  20245  dprdres  20253  dmdprdsplitlem  20262  dprdcntz2  20263  dmdprdsplit2lem  20270  dprdsplit  20273  dpjidcl  20283  ablfac1eu  20298  rngmgpf  20388  mgpf  20484  prdscrngd  20560  abvres  21097  reslmhm  21336  znf1o  21866  znunithash  21879  ltbwe  22362  subrgascl  22384  subrgasclcl  22385  smadiadetlem3  22992  lmres  23627  tx1cn  23937  tx2cn  23938  ptrescn  23967  cnmpt1st  23996  cnmpt2nd  23997  ptuncnv  24135  ptunhmeo  24136  cnextfres1  24396  prdstmdd  24452  prdsxmslem2  24857  subgnm2  24962  rescncf  25227  isncvsngp  25479  lmle  25631  ovoliunlem1  25832  ovolicc2lem4  25850  mblvol  25860  mbflimsup  25996  limcdif  26205  limcres  26215  dvres2lem  26239  dvlip  26322  dvlipcn  26323  dvlip2  26324  c1liplem1  26325  c1lip1  26326  c1lip3  26328  dvivthlem1  26337  lhop1lem  26342  lhop  26345  dvcvx  26349  ftc2ditglem  26374  itgsubstlem  26377  plyreres  26613  plyexmo  26645  aannenlem1  26664  taylthlem2  26710  ulmres  26724  ulmss  26733  pserdvlem2  26764  reeff1o  26783  reefiso  26784  reefgim  26786  recosf1o  26872  resinf1o  26873  relogcl  26912  logef  26918  logeftb  26920  logltb  26937  logcn  26984  advlog  26991  advlogexp  26992  logtayl  26997  logccv  27000  dvcxp1  27077  dvcncxp1  27080  cxpcn  27082  loglesqrt  27098  dvatan  27272  leibpi  27279  efrlim  27306  amgmlem  27326  lgamgulmlem2  27366  lgamcvg2  27391  wilthlem3  27406  ftalem3  27411  mpodvdsmulf1o  27530  fsumdvdsmul  27531  dvdsmulf1o  27532  dchrelbas2  27573  dchrabs  27596  dchrisumlem1  27825  logdivsum  27869  log2sumbnd  27880  ostth2  27973  ostth  27975  ltsres  28028  nodense  28058  nolt02o  28061  nogt01o  28062  noetainflem4  28106  oniso  28666  bdayn0sf1o  28765  vtxdginducedm1lem3  30131  redwlk  30260  pthdivtx  30321  pthdlem1  30361  ex-fpar  31072  sspnval  31348  hhssnv  31875  hhssmetdval  31888  foresf1o  33151  1stpreimas  33350  cos9thpiminply  34470  xpinpreima  34588  xpinpreima2  34589  cnre2csqlem  34592  zzsnm  34641  cnzh  34650  rezh  34651  measres  34905  cntmeas  34909  cntnevol  34911  1stmbfm  34942  2ndmbfm  34943  carsggect  35000  omsmeas  35005  eulerpartgbij  35054  eulerpartlemgvv  35058  eulerpartlemgs2  35062  iwrdsplit  35069  fibp1  35083  coinfliplem  35161  coinflipprob  35162  gsumnunsn  35223  plyrecld  35228  signstres  35254  ftc2re  35277  bnj1253  35697  bnj1280  35700  fwfffunres  35768  noinfepregs  35861  gblacfnacd  35952  subfacp1lem3  36037  subfacp1lem5  36039  erdszelem8  36053  txsconnlem  36095  cvmfolem  36134  cvmliftmolem1  36136  cvmliftlem6  36145  cvmliftlem7  36146  cvmliftlem9  36148  satfsucom  36209  satom  36211  satfvsucom  36212  satf0sucom  36228  mrsubff1  36369  msubff1  36411  dfrdg2  36653  funpartfv  36805  filnetlem4  37265  icoreunrn  38391  finixpnum  38637  poimirlem3  38650  poimirlem4  38651  poimirlem8  38655  poimirlem26  38673  poimirlem27  38674  itg2gt0cn  38702  areacirclem2  38736  areacirclem4  38738  sdclem2  38785  caures  38803  ismtyres  38851  diaintclN  42224  dibintclN  42333  dihintcl  42510  fsuppssindlem1  43728  imaiinfv  43813  mzpcompact2lem  43871  2rexfrabdioph  43912  3rexfrabdioph  43913  4rexfrabdioph  43914  6rexfrabdioph  43915  7rexfrabdioph  43916  jm2.27dlem1  44125  aomclem6  44170  deg1mhm  44311  hausgraph  44316  radcnvrat  45407  hashnna  46117  hashomiso  46123  wessf1ornlem  46308  feqresmptf  46351  mccllem  46717  limcleqr  46762  limsupvaluz2  46856  supcnvlimsup  46858  limsupgtlem  46895  xlimconst2  46953  resincncf  46993  cncfperiod  46997  icccncfext  47005  cncfiooicclem1  47011  dvbdfbdioolem1  47046  dvnprodlem1  47064  dvnprodlem2  47065  itgioocnicc  47095  stoweidlem28  47146  fourierdlem18  47243  fourierdlem40  47265  fourierdlem42  47267  fourierdlem46  47270  fourierdlem51  47275  fourierdlem70  47294  fourierdlem71  47295  fourierdlem73  47297  fourierdlem74  47298  fourierdlem75  47299  fourierdlem76  47300  fourierdlem78  47302  fourierdlem80  47304  fourierdlem81  47305  fourierdlem82  47306  fourierdlem84  47308  fourierdlem89  47313  fourierdlem90  47314  fourierdlem91  47315  fourierdlem92  47316  fourierdlem93  47317  fourierdlem94  47318  fourierdlem101  47325  fourierdlem103  47327  fourierdlem104  47328  fourierdlem111  47335  fourierdlem112  47336  fourierdlem113  47337  sge0tsms  47498  sge0f1o  47500  sge0sup  47509  sge0less  47510  sge0ltfirp  47518  sge0resrnlem  47521  sge0resplit  47524  sge0le  47525  sge0split  47527  sge0fodjrnlem  47534  sge0iun  47537  meadjun  47580  meadjiunlem  47583  psmeasurelem  47588  caratheodory  47646  hoidmvlelem2  47714  hoidmvlelem3  47715  hoidmvlelem4  47716  voncmpl  47739  mblvon  47757  smflimsuplem3  47940  cjnpoly  48047  sqrtrrnpoly  48050  afvres  48350  iccpartres  48608  iccelpart  48623  isubgredg  49072  isubgrgrim  49135  uhgrimisgrgric  49137  lincdifsn  49644  lindslinindimp2lem4  49681  lindslinindsimp2lem5  49682  lincresunit3lem2  49700  fdivmpt  49760  slotresfo  50121  basresposfo  50200  oppff1  50372  setrecsres  50978  amgmwlem  51170