Theorem fvres 6859

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 3448	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5948	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6483	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6507	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6507	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2789	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   class class class wbr 5102   ↾ cres 5633  ℩cio 6450  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-res 5643  df-iota 6452  df-fv 6507

This theorem is referenced by:  fvresd  6860  funssfv  6861  fveqres  6887  feqresmpt  6912  dffv2  6938  eqfnun  6991  fvreseq0  6992  respreima  7020  fveqressseq  7033  ffvresb  7079  fnressn  7112  fressnfv  7114  fvresi  7129  funfvima  7186  funiunfv  7204  soisores  7284  isores3  7292  isoini2  7296  fvresval  7315  ofres  7652  f1oweALT  7930  offres  7941  fo1stres  7973  fo2ndres  7974  fparlem1  8068  fparlem2  8069  fsplitfpar  8074  fo2ndf  8077  f1o2ndf1  8078  fnsuppres  8147  tfrlem1  8321  fr0g  8381  frsuc  8382  tz7.48lem  8386  seqomlem1  8395  seqomlem2  8396  seqomlem3  8397  seqomlem4  8398  onasuc  8469  onmsuc  8470  onesuc  8471  resixp  8883  fofinf1o  9259  ixpfi2  9277  ttrclss  9649  updjudhcoinlf  9861  updjudhcoinrg  9862  updjud  9863  ackbij2lem2  10168  ackbij2lem3  10169  cfsmolem  10199  alephsing  10205  fpwwe2lem7  10566  inar1  10704  addpiord  10813  mulpiord  10814  fseq1p1m1  13535  injresinj  13725  seqfeq2  13966  seqres  13970  seqf1olem2  13983  hashgval  14274  hashinf  14276  hashgval2  14319  hashf1lem1  14396  pfxccat1  14643  shftidt  15024  climres  15517  fsumss  15667  isumclim3  15701  fsum2dlem  15712  ackbijnn  15770  fprodss  15890  fprod2dlem  15922  iprodclim3  15942  bpolylem  15990  fprodefsum  16037  reeff1  16064  bitsf1  16392  sadcadd  16404  sadadd2  16406  eucalgcvga  16532  eucalg  16533  unbenlem  16855  strfv2d  17147  setsid  17153  setsnid  17154  dfinito3  17943  dftermo3  17944  dmaf  17987  cdaf  17988  1stfcl  18134  2ndfcl  18135  resmgmhm  18614  resmhm  18723  resghm  19140  efgredlem  19653  gsumzaddlem  19827  dprdfadd  19928  dprdres  19936  dmdprdsplitlem  19945  dprdcntz2  19946  dmdprdsplit2lem  19953  dprdsplit  19956  dpjidcl  19966  ablfac1eu  19981  rngmgpf  20042  mgpf  20133  prdscrngd  20207  abvres  20716  reslmhm  20935  znf1o  21437  znunithash  21450  ltbwe  21927  subrgascl  21949  subrgasclcl  21950  smadiadetlem3  22531  lmres  23163  tx1cn  23472  tx2cn  23473  ptrescn  23502  cnmpt1st  23531  cnmpt2nd  23532  ptuncnv  23670  ptunhmeo  23671  cnextfres1  23931  prdstmdd  23987  prdsxmslem2  24393  subgnm2  24498  rescncf  24766  isncvsngp  25025  lmle  25177  ovoliunlem1  25379  ovolicc2lem4  25397  mblvol  25407  mbflimsup  25543  limcdif  25753  limcres  25763  dvres2lem  25787  dvlip  25874  dvlipcn  25875  dvlip2  25876  c1liplem1  25877  c1lip1  25878  c1lip3  25880  dvivthlem1  25889  lhop1lem  25894  lhop  25897  dvcvx  25901  ftc2ditglem  25928  itgsubstlem  25931  plyreres  26166  plyexmo  26197  aannenlem1  26212  taylthlem2  26258  taylthlem2OLD  26259  ulmres  26273  ulmss  26282  pserdvlem2  26314  reeff1o  26333  reefiso  26334  reefgim  26336  recosf1o  26420  resinf1o  26421  relogcl  26460  logef  26466  logeftb  26468  logltb  26485  logcn  26532  advlog  26539  advlogexp  26540  logtayl  26545  logccv  26548  dvcxp1  26625  dvcncxp1  26628  cxpcn  26630  cxpcnOLD  26631  loglesqrt  26647  dvatan  26821  leibpi  26828  efrlim  26855  efrlimOLD  26856  amgmlem  26876  lgamgulmlem2  26916  lgamcvg2  26941  wilthlem3  26956  ftalem3  26961  mpodvdsmulf1o  27080  fsumdvdsmul  27081  dvdsmulf1o  27082  fsumdvdsmulOLD  27083  dchrelbas2  27124  dchrabs  27147  dchrisumlem1  27376  logdivsum  27420  log2sumbnd  27431  ostth2  27524  ostth  27526  sltres  27550  nodense  27580  nolt02o  27583  nogt01o  27584  noetainflem4  27628  onsiso  28145  bdayn0sf1o  28235  vtxdginducedm1lem3  29445  redwlk  29574  pthdivtx  29630  pthdlem1  29669  ex-fpar  30364  sspnval  30639  hhssnv  31166  hhssmetdval  31179  foresf1o  32406  1stpreimas  32602  cos9thpiminply  33751  xpinpreima  33869  xpinpreima2  33870  cnre2csqlem  33873  zzsnm  33922  cnzh  33931  rezh  33932  measres  34185  cntmeas  34189  cntnevol  34191  1stmbfm  34224  2ndmbfm  34225  carsggect  34282  omsmeas  34287  eulerpartgbij  34336  eulerpartlemgvv  34340  eulerpartlemgs2  34344  iwrdsplit  34351  fibp1  34365  coinfliplem  34443  coinflipprob  34444  gsumnunsn  34505  plyrecld  34513  signstres  34539  ftc2re  34562  bnj1253  34980  bnj1280  34983  f1resveqaeq  35048  gblacfnacd  35062  subfacp1lem3  35142  subfacp1lem5  35144  erdszelem8  35158  txsconnlem  35200  cvmfolem  35239  cvmliftmolem1  35241  cvmliftlem6  35250  cvmliftlem7  35251  cvmliftlem9  35253  satfsucom  35314  satom  35316  satfvsucom  35317  satf0sucom  35333  mrsubff1  35474  msubff1  35516  dfrdg2  35756  funpartfv  35906  filnetlem4  36342  icoreunrn  37320  finixpnum  37572  poimirlem3  37590  poimirlem4  37591  poimirlem8  37595  poimirlem26  37613  poimirlem27  37614  itg2gt0cn  37642  areacirclem2  37676  areacirclem4  37678  sdclem2  37709  caures  37727  ismtyres  37775  diaintclN  41025  dibintclN  41134  dihintcl  41311  fsuppssindlem1  42552  imaiinfv  42654  mzpcompact2lem  42712  2rexfrabdioph  42757  3rexfrabdioph  42758  4rexfrabdioph  42759  6rexfrabdioph  42760  7rexfrabdioph  42761  jm2.27dlem1  42971  fnwe2lem2  43013  aomclem6  43021  deg1mhm  43162  hausgraph  43167  radcnvrat  44276  wessf1ornlem  45152  feqresmptf  45198  mccllem  45568  limcleqr  45615  limsupvaluz2  45709  supcnvlimsup  45711  limsupgtlem  45748  xlimconst2  45806  resincncf  45846  cncfperiod  45850  icccncfext  45858  cncfiooicclem1  45864  dvbdfbdioolem1  45899  dvnprodlem1  45917  dvnprodlem2  45918  itgioocnicc  45948  stoweidlem28  45999  fourierdlem18  46096  fourierdlem40  46118  fourierdlem42  46120  fourierdlem46  46123  fourierdlem51  46128  fourierdlem70  46147  fourierdlem71  46148  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem78  46155  fourierdlem80  46157  fourierdlem81  46158  fourierdlem82  46159  fourierdlem84  46161  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem92  46169  fourierdlem93  46170  fourierdlem94  46171  fourierdlem101  46178  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem112  46189  fourierdlem113  46190  sge0tsms  46351  sge0f1o  46353  sge0sup  46362  sge0less  46363  sge0ltfirp  46371  sge0resrnlem  46374  sge0resplit  46377  sge0le  46378  sge0split  46380  sge0fodjrnlem  46387  sge0iun  46390  meadjun  46433  meadjiunlem  46436  psmeasurelem  46441  caratheodory  46499  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  voncmpl  46592  mblvon  46610  smflimsuplem3  46793  cjnpoly  46863  afvres  47146  iccpartres  47392  iccelpart  47407  isubgredg  47839  isubgrgrim  47902  uhgrimisgrgric  47904  lincdifsn  48386  lindslinindimp2lem4  48423  lindslinindsimp2lem5  48424  lincresunit3lem2  48442  fdivmpt  48502  slotresfo  48860  basresposfo  48939  oppff1  49110  setrec2lem1  49655  setrecsres  49664  amgmwlem  49764