Theorem fvres 6117

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 3176	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brres 5323	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴𝐹𝑥 ∧ 𝐴 ∈ 𝐵))
3	2	rbaib 945	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 5789	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 5812	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 5812	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2669	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   class class class wbr 4583   ↾ cres 5040  ℩cio 5766  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-res 5050  df-iota 5768  df-fv 5812

This theorem is referenced by:  fvresd  6118  funssfv  6119  fveqres  6140  feqresmpt  6160  dffv2  6181  fvreseq0  6225  respreima  6252  fveqressseq  6263  ffvresb  6301  fnressn  6330  fressnfv  6332  fvressn  6334  fvresi  6344  fvsnun1  6353  fvsnun2  6354  fsnunfv  6358  funfvima  6396  resfvresima  6398  funiunfv  6410  soisores  6477  isores3  6485  isoini2  6489  ovres  6698  ofres  6811  f1oweALT  7043  offres  7054  fo1stres  7083  fo2ndres  7084  curry1  7156  curry2  7159  fparlem1  7164  fparlem2  7165  fo2ndf  7171  f1o2ndf1  7172  fnsuppres  7209  wfrlem4  7305  smores  7336  smores2  7338  tfrlem1  7359  tz7.44-2  7390  fr0g  7418  frsuc  7419  tz7.48lem  7423  seqomlem1  7432  seqomlem2  7433  seqomlem3  7434  seqomlem4  7435  onasuc  7495  onmsuc  7496  onesuc  7497  resixp  7829  fofinf1o  8126  ixpfi2  8147  ordtypelem4  8309  ordtypelem6  8311  ordtypelem7  8312  unxpwdom2  8376  cantnfres  8457  cantnfp1lem3  8460  dfac12lem1  8848  ackbij2lem2  8945  ackbij2lem3  8946  cfsmolem  8975  alephsing  8981  ttukeylem3  9216  fpwwe2lem6  9336  fpwwe2lem8  9338  fpwwe2lem9  9339  canthp1lem2  9354  inar1  9476  addpiord  9585  mulpiord  9586  addpqnq  9639  mulpqnq  9642  fseq1p1m1  12283  injresinj  12451  seqfeq2  12686  seqres  12690  seqf1olem2  12703  hashgval  12982  hashinf  12984  hashgval2  13028  hashf1lem1  13096  seqcoll  13105  swrdccat1  13309  shftidt  13670  rlimres  14137  lo1res  14138  climres  14154  isercolllem3  14245  fsumss  14303  isumclim3  14332  fsum2dlem  14343  ackbijnn  14399  fprodss  14517  fprod2dlem  14549  iprodclim3  14570  bpolylem  14618  fprodefsum  14664  reeff1  14689  bitsf1  15006  sadcaddlem  15017  sadcadd  15018  sadadd2  15020  sadaddlem  15026  sadasslem  15030  sadeq  15032  eucalgcvga  15137  eucalg  15138  unbenlem  15450  strfv2d  15733  setsid  15742  setsnid  15743  funcres  16379  dmaf  16522  cdaf  16523  1stf1  16655  2ndf1  16658  1stfcl  16660  2ndfcl  16661  prf1st  16667  prf2nd  16668  1st2ndprf  16669  uncf2  16700  diag12  16707  diag2  16708  curf2ndf  16710  yonedalem22  16741  lubval  16807  glbval  16820  resmhm  17182  resghm  17499  efgsres  17974  efgredlemd  17980  efgredlem  17983  gsumzaddlem  18144  dprdfadd  18242  dprdres  18250  dmdprdsplitlem  18259  dprdcntz2  18260  dmdprdsplit2lem  18267  dprdsplit  18270  dpjidcl  18280  ablfac1eu  18295  mgpf  18382  prdscrngd  18436  abvres  18662  reslmhm  18873  ltbwe  19293  subrgascl  19319  subrgasclcl  19320  znf1o  19719  znunithash  19732  psgndiflemB  19765  smadiadetlem3  20293  cnpresti  20902  cnprest  20903  lmres  20914  tx1cn  21222  tx2cn  21223  upxp  21236  uptx  21238  ptrescn  21252  cnmpt1st  21281  cnmpt2nd  21282  ptuncnv  21420  ptunhmeo  21421  cnextfres1  21682  prdstmdd  21737  prdsxmslem2  22144  subgnm2  22248  remetdval  22400  rescncf  22508  isncvsngp  22757  lmle  22907  lmcau  22919  ovoliunlem1  23077  ovolicc2lem4  23095  mblvol  23105  mbflimsup  23239  limcdif  23446  limcres  23456  dvreslem  23479  dvres2lem  23480  dvlip  23560  dvlipcn  23561  dvlip2  23562  c1liplem1  23563  c1lip1  23564  c1lip3  23566  dvgt0lem1  23569  dvivthlem1  23575  lhop1lem  23580  lhop  23583  dvcnvrelem1  23584  dvcvx  23587  ftc2ditglem  23612  itgsubstlem  23615  plyreres  23842  plyexmo  23872  aannenlem1  23887  taylthlem2  23932  ulmres  23946  ulmss  23955  psercn  23984  pserdvlem2  23986  reeff1o  24005  reefiso  24006  efcvx  24007  reefgim  24008  recosf1o  24085  resinf1o  24086  efif1olem4  24095  eff1olem  24098  relogcl  24126  eflog  24127  logef  24132  logeftb  24134  logltb  24150  logcn  24193  advlog  24200  advlogexp  24201  logtayl  24206  logccv  24209  dvcxp1  24281  dvcncxp1  24284  cxpcn  24286  loglesqrt  24299  asinrebnd  24428  dvatan  24462  leibpi  24469  efrlim  24496  jensen  24515  amgmlem  24516  lgamgulmlem2  24556  lgamcvg2  24581  wilthlem3  24596  ftalem3  24601  dvdsmulf1o  24720  fsumdvdsmul  24721  dchrelbas2  24762  dchrabs  24785  sum2dchr  24799  dchrisumlem1  24978  logdivsum  25022  log2sumbnd  25033  ostth2  25126  ostth  25128  redwlk  26136  eupares  26502  sspnval  26976  hhssnv  27505  hhssmetdval  27519  foresf1o  28727  ofresid  28824  1stpreimas  28866  xpinpreima  29280  xpinpreima2  29281  cnre2csqlem  29284  rmulccn  29302  zzsnm  29333  cnzh  29342  rezh  29343  measres  29612  cntmeas  29616  cntnevol  29618  1stmbfm  29649  2ndmbfm  29650  carsggect  29707  omsmeas  29712  eulerpartgbij  29761  eulerpartlemgvv  29765  eulerpartlemgs2  29769  iwrdsplit  29776  fibp1  29790  coinfliplem  29867  coinflipprob  29868  gsumnunsn  29942  plyrecld  29952  signstres  29978  bnj1379  30155  bnj1253  30339  bnj1280  30342  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem8  30434  txsconlem  30476  cvmfolem  30515  cvmliftmolem1  30517  cvmliftlem6  30526  cvmliftlem7  30527  cvmliftlem9  30529  mrsubff1  30665  msubff1  30707  fvresval  30911  dfrdg2  30945  frrlem4  31027  sltres  31061  nodense  31088  funpartfv  31222  filnetlem4  31546  icoreunrn  32383  finixpnum  32564  poimirlem3  32582  poimirlem4  32583  poimirlem8  32587  poimirlem26  32605  poimirlem27  32606  itg2gt0cn  32635  areacirclem2  32671  areacirclem4  32673  eqfnun  32686  sdclem2  32708  caures  32726  ismtyres  32777  diaintclN  35365  dibintclN  35474  dihintcl  35651  imaiinfv  36274  mzpcompact2lem  36332  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  jm2.27dlem1  36594  fnwe2lem2  36639  fnwe2lem3  36640  aomclem6  36647  deg1mhm  36804  hausgraph  36809  radcnvrat  37535  wessf1ornlem  38366  mccllem  38664  limcperiod  38695  limcleqr  38711  limclner  38718  resincncf  38760  cncfperiod  38764  icccncfext  38773  cncfiooicclem1  38779  dvbdfbdioolem1  38818  dvnprodlem1  38836  dvnprodlem2  38837  itgioocnicc  38869  stoweidlem28  38921  fourierdlem18  39018  fourierdlem40  39040  fourierdlem42  39042  fourierdlem46  39045  fourierdlem51  39050  fourierdlem70  39069  fourierdlem71  39070  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem80  39079  fourierdlem81  39080  fourierdlem82  39081  fourierdlem84  39083  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem94  39093  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  sge0tsms  39273  sge0f1o  39275  sge0sup  39284  sge0less  39285  sge0ltfirp  39293  sge0resrnlem  39296  sge0resplit  39299  sge0le  39300  sge0split  39302  sge0fodjrnlem  39309  sge0iun  39312  meadjun  39355  meadjiunlem  39358  psmeasurelem  39363  caratheodory  39418  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  voncmpl  39511  mblvon  39529  afvres  39901  iccpartres  39956  iccelpart  39971  pfxccat1  40273  uhgrspansubgrlem  40514  1wlkres  40879  red1wlk  40881  pthdivtx  40935  pthdlem1  40972  resmgmhm  41588  rhmsubclem2  41879  rhmsubcALTVlem2  41898  lincdifsn  42007  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  lincresunit3lem2  42063  fdivmpt  42132  setrec2lem1  42239  amgmwlem  42357