Theorem fvres 6560

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 3439	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5746	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 536	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6213	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6236	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6236	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2855	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2080   class class class wbr 4964   ↾ cres 5448  ℩cio 6190  ‘cfv 6228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pr 5224

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-br 4965  df-opab 5027  df-xp 5452  df-res 5458  df-iota 6192  df-fv 6236

This theorem is referenced by:  fvresd  6561  funssfv  6562  fveqres  6583  feqresmpt  6605  dffv2  6626  fvreseq0  6676  respreima  6704  fveqressseq  6715  ffvresb  6754  fnressn  6786  fressnfv  6788  fvresi  6801  fvsnun1OLD  6814  fvsnun2OLD  6815  funfvima  6861  funiunfv  6875  soisores  6946  isores3  6954  isoini2  6958  ofres  7286  f1oweALT  7532  offres  7543  fo1stres  7574  fo2ndres  7575  fparlem1  7666  fparlem2  7667  fo2ndf  7673  f1o2ndf1  7674  fnsuppres  7711  wfrlem4  7812  wfrlem4OLD  7813  tfrlem1  7867  fr0g  7926  frsuc  7927  tz7.48lem  7931  seqomlem1  7940  seqomlem2  7941  seqomlem3  7942  seqomlem4  7943  onasuc  8007  onmsuc  8008  onesuc  8009  resixp  8348  fofinf1o  8648  ixpfi2  8671  updjudhcoinlf  9210  updjudhcoinrg  9211  updjud  9212  ackbij2lem2  9511  ackbij2lem3  9512  cfsmolem  9541  alephsing  9547  fpwwe2lem8  9908  inar1  10046  addpiord  10155  mulpiord  10156  fseq1p1m1  12831  injresinj  13008  seqfeq2  13243  seqres  13247  seqf1olem2  13260  hashgval  13543  hashinf  13545  hashgval2  13587  hashf1lem1  13661  pfxccat1  13900  shftidt  14275  climres  14766  fsumss  14915  isumclim3  14947  fsum2dlem  14958  ackbijnn  15016  fprodss  15135  fprod2dlem  15167  iprodclim3  15187  bpolylem  15235  fprodefsum  15281  reeff1  15306  bitsf1  15628  sadcadd  15640  sadadd2  15642  eucalgcvga  15759  eucalg  15760  unbenlem  16073  strfv2d  16358  setsid  16367  setsnid  16368  dmaf  17138  cdaf  17139  1stfcl  17276  2ndfcl  17277  resmhm  17798  resghm  18115  efgredlem  18600  gsumzaddlem  18761  dprdfadd  18859  dprdres  18867  dmdprdsplitlem  18876  dprdcntz2  18877  dmdprdsplit2lem  18884  dprdsplit  18887  dpjidcl  18897  ablfac1eu  18912  mgpf  18999  prdscrngd  19053  abvres  19300  reslmhm  19514  ltbwe  19940  subrgascl  19965  subrgasclcl  19966  znf1o  20380  znunithash  20393  smadiadetlem3  20961  lmres  21592  tx1cn  21901  tx2cn  21902  ptrescn  21931  cnmpt1st  21960  cnmpt2nd  21961  ptuncnv  22099  ptunhmeo  22100  cnextfres1  22360  prdstmdd  22415  prdsxmslem2  22822  subgnm2  22926  rescncf  23188  isncvsngp  23436  lmle  23587  ovoliunlem1  23786  ovolicc2lem4  23804  mblvol  23814  mbflimsup  23950  limcdif  24157  limcres  24167  dvres2lem  24191  dvlip  24273  dvlipcn  24274  dvlip2  24275  c1liplem1  24276  c1lip1  24277  c1lip3  24279  dvivthlem1  24288  lhop1lem  24293  lhop  24296  dvcvx  24300  ftc2ditglem  24325  itgsubstlem  24328  plyreres  24555  plyexmo  24585  aannenlem1  24600  taylthlem2  24645  ulmres  24659  ulmss  24668  pserdvlem2  24699  reeff1o  24718  reefiso  24719  reefgim  24721  recosf1o  24800  resinf1o  24801  relogcl  24840  logef  24846  logeftb  24848  logltb  24864  logcn  24911  advlog  24918  advlogexp  24919  logtayl  24924  logccv  24927  dvcxp1  25002  dvcncxp1  25005  cxpcn  25007  loglesqrt  25020  dvatan  25194  leibpi  25202  efrlim  25229  amgmlem  25249  lgamgulmlem2  25289  lgamcvg2  25314  wilthlem3  25329  ftalem3  25334  dvdsmulf1o  25453  fsumdvdsmul  25454  dchrelbas2  25495  dchrabs  25518  dchrisumlem1  25747  logdivsum  25791  log2sumbnd  25802  ostth2  25895  ostth  25897  vtxdginducedm1lem3  27006  redwlk  27136  pthdivtx  27192  pthdlem1  27229  sspnval  28197  hhssnv  28724  hhssmetdval  28737  foresf1o  29949  1stpreimas  30121  xpinpreima  30758  xpinpreima2  30759  cnre2csqlem  30762  rmulccn  30780  zzsnm  30811  cnzh  30820  rezh  30821  measres  31090  cntmeas  31094  cntnevol  31096  1stmbfm  31127  2ndmbfm  31128  carsggect  31185  omsmeas  31190  eulerpartgbij  31239  eulerpartlemgvv  31243  eulerpartlemgs2  31247  iwrdsplit  31254  fibp1  31268  coinfliplem  31345  coinflipprob  31346  gsumnunsn  31420  plyrecld  31428  signstres  31454  ftc2re  31478  bnj1253  31895  bnj1280  31898  f1resveqaeq  31964  subfacp1lem3  32031  subfacp1lem5  32033  erdszelem8  32047  txsconnlem  32089  cvmfolem  32128  cvmliftmolem1  32130  cvmliftlem6  32139  cvmliftlem7  32140  cvmliftlem9  32142  satfsucom  32203  satom  32205  satfvsucom  32206  satf0sucom  32222  mrsubff1  32363  msubff1  32405  fvresval  32612  dfrdg2  32643  sltres  32772  nodense  32799  nolt02o  32802  funpartfv  33009  filnetlem4  33332  icoreunrn  34184  finixpnum  34421  poimirlem3  34439  poimirlem4  34440  poimirlem8  34444  poimirlem26  34462  poimirlem27  34463  itg2gt0cn  34491  areacirclem2  34527  areacirclem4  34529  eqfnun  34542  sdclem2  34562  caures  34580  ismtyres  34631  diaintclN  37738  dibintclN  37847  dihintcl  38024  imaiinfv  38788  mzpcompact2lem  38846  2rexfrabdioph  38891  3rexfrabdioph  38892  4rexfrabdioph  38893  6rexfrabdioph  38894  7rexfrabdioph  38895  jm2.27dlem1  39104  fnwe2lem2  39149  aomclem6  39157  deg1mhm  39305  hausgraph  39310  radcnvrat  40197  wessf1ornlem  40998  feqresmptf  41052  mccllem  41433  limcleqr  41480  limsupvaluz2  41574  supcnvlimsup  41576  limsupgtlem  41613  xlimconst2  41671  resincncf  41713  cncfperiod  41717  icccncfext  41725  cncfiooicclem1  41731  dvbdfbdioolem1  41768  dvnprodlem1  41786  dvnprodlem2  41787  itgioocnicc  41817  stoweidlem28  41869  fourierdlem18  41966  fourierdlem40  41988  fourierdlem42  41990  fourierdlem46  41993  fourierdlem51  41998  fourierdlem70  42017  fourierdlem71  42018  fourierdlem73  42020  fourierdlem74  42021  fourierdlem75  42022  fourierdlem76  42023  fourierdlem78  42025  fourierdlem80  42027  fourierdlem81  42028  fourierdlem82  42029  fourierdlem84  42031  fourierdlem89  42036  fourierdlem90  42037  fourierdlem91  42038  fourierdlem92  42039  fourierdlem93  42040  fourierdlem94  42041  fourierdlem101  42048  fourierdlem103  42050  fourierdlem104  42051  fourierdlem111  42058  fourierdlem112  42059  fourierdlem113  42060  sge0tsms  42218  sge0f1o  42220  sge0sup  42229  sge0less  42230  sge0ltfirp  42238  sge0resrnlem  42241  sge0resplit  42244  sge0le  42245  sge0split  42247  sge0fodjrnlem  42254  sge0iun  42257  meadjun  42300  meadjiunlem  42303  psmeasurelem  42308  caratheodory  42366  hoidmvlelem2  42434  hoidmvlelem3  42435  hoidmvlelem4  42436  voncmpl  42459  mblvon  42477  smflimsuplem3  42652  afvres  42901  iccpartres  43074  iccelpart  43089  resmgmhm  43561  lincdifsn  43973  lindslinindimp2lem4  44010  lindslinindsimp2lem5  44011  lincresunit3lem2  44029  fdivmpt  44095  setrec2lem1  44290  setrecsres  44298  amgmwlem  44397