Theorem fvres 6880

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 5962	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6498	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6522	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6522	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2790	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   class class class wbr 5110   ↾ cres 5643  ℩cio 6465  ‘cfv 6514

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-res 5653  df-iota 6467  df-fv 6522

This theorem is referenced by:  fvresd  6881  funssfv  6882  fveqres  6908  feqresmpt  6933  dffv2  6959  eqfnun  7012  fvreseq0  7013  respreima  7041  fveqressseq  7054  ffvresb  7100  fnressn  7133  fressnfv  7135  fvresi  7150  funfvima  7207  funiunfv  7225  soisores  7305  isores3  7313  isoini2  7317  fvresval  7336  ofres  7675  f1oweALT  7954  offres  7965  fo1stres  7997  fo2ndres  7998  fparlem1  8094  fparlem2  8095  fsplitfpar  8100  fo2ndf  8103  f1o2ndf1  8104  fnsuppres  8173  tfrlem1  8347  fr0g  8407  frsuc  8408  tz7.48lem  8412  seqomlem1  8421  seqomlem2  8422  seqomlem3  8423  seqomlem4  8424  onasuc  8495  onmsuc  8496  onesuc  8497  resixp  8909  fofinf1o  9290  ixpfi2  9308  ttrclss  9680  updjudhcoinlf  9892  updjudhcoinrg  9893  updjud  9894  ackbij2lem2  10199  ackbij2lem3  10200  cfsmolem  10230  alephsing  10236  fpwwe2lem7  10597  inar1  10735  addpiord  10844  mulpiord  10845  fseq1p1m1  13566  injresinj  13756  seqfeq2  13997  seqres  14001  seqf1olem2  14014  hashgval  14305  hashinf  14307  hashgval2  14350  hashf1lem1  14427  pfxccat1  14674  shftidt  15055  climres  15548  fsumss  15698  isumclim3  15732  fsum2dlem  15743  ackbijnn  15801  fprodss  15921  fprod2dlem  15953  iprodclim3  15973  bpolylem  16021  fprodefsum  16068  reeff1  16095  bitsf1  16423  sadcadd  16435  sadadd2  16437  eucalgcvga  16563  eucalg  16564  unbenlem  16886  strfv2d  17178  setsid  17184  setsnid  17185  dfinito3  17974  dftermo3  17975  dmaf  18018  cdaf  18019  1stfcl  18165  2ndfcl  18166  resmgmhm  18645  resmhm  18754  resghm  19171  efgredlem  19684  gsumzaddlem  19858  dprdfadd  19959  dprdres  19967  dmdprdsplitlem  19976  dprdcntz2  19977  dmdprdsplit2lem  19984  dprdsplit  19987  dpjidcl  19997  ablfac1eu  20012  rngmgpf  20073  mgpf  20164  prdscrngd  20238  abvres  20747  reslmhm  20966  znf1o  21468  znunithash  21481  ltbwe  21958  subrgascl  21980  subrgasclcl  21981  smadiadetlem3  22562  lmres  23194  tx1cn  23503  tx2cn  23504  ptrescn  23533  cnmpt1st  23562  cnmpt2nd  23563  ptuncnv  23701  ptunhmeo  23702  cnextfres1  23962  prdstmdd  24018  prdsxmslem2  24424  subgnm2  24529  rescncf  24797  isncvsngp  25056  lmle  25208  ovoliunlem1  25410  ovolicc2lem4  25428  mblvol  25438  mbflimsup  25574  limcdif  25784  limcres  25794  dvres2lem  25818  dvlip  25905  dvlipcn  25906  dvlip2  25907  c1liplem1  25908  c1lip1  25909  c1lip3  25911  dvivthlem1  25920  lhop1lem  25925  lhop  25928  dvcvx  25932  ftc2ditglem  25959  itgsubstlem  25962  plyreres  26197  plyexmo  26228  aannenlem1  26243  taylthlem2  26289  taylthlem2OLD  26290  ulmres  26304  ulmss  26313  pserdvlem2  26345  reeff1o  26364  reefiso  26365  reefgim  26367  recosf1o  26451  resinf1o  26452  relogcl  26491  logef  26497  logeftb  26499  logltb  26516  logcn  26563  advlog  26570  advlogexp  26571  logtayl  26576  logccv  26579  dvcxp1  26656  dvcncxp1  26659  cxpcn  26661  cxpcnOLD  26662  loglesqrt  26678  dvatan  26852  leibpi  26859  efrlim  26886  efrlimOLD  26887  amgmlem  26907  lgamgulmlem2  26947  lgamcvg2  26972  wilthlem3  26987  ftalem3  26992  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  dchrelbas2  27155  dchrabs  27178  dchrisumlem1  27407  logdivsum  27451  log2sumbnd  27462  ostth2  27555  ostth  27557  sltres  27581  nodense  27611  nolt02o  27614  nogt01o  27615  noetainflem4  27659  onsiso  28176  bdayn0sf1o  28266  vtxdginducedm1lem3  29476  redwlk  29607  pthdivtx  29664  pthdlem1  29703  ex-fpar  30398  sspnval  30673  hhssnv  31200  hhssmetdval  31213  foresf1o  32440  1stpreimas  32636  cos9thpiminply  33785  xpinpreima  33903  xpinpreima2  33904  cnre2csqlem  33907  zzsnm  33956  cnzh  33965  rezh  33966  measres  34219  cntmeas  34223  cntnevol  34225  1stmbfm  34258  2ndmbfm  34259  carsggect  34316  omsmeas  34321  eulerpartgbij  34370  eulerpartlemgvv  34374  eulerpartlemgs2  34378  iwrdsplit  34385  fibp1  34399  coinfliplem  34477  coinflipprob  34478  gsumnunsn  34539  plyrecld  34547  signstres  34573  ftc2re  34596  bnj1253  35014  bnj1280  35017  f1resveqaeq  35082  gblacfnacd  35096  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem8  35192  txsconnlem  35234  cvmfolem  35273  cvmliftmolem1  35275  cvmliftlem6  35284  cvmliftlem7  35285  cvmliftlem9  35287  satfsucom  35348  satom  35350  satfvsucom  35351  satf0sucom  35367  mrsubff1  35508  msubff1  35550  dfrdg2  35790  funpartfv  35940  filnetlem4  36376  icoreunrn  37354  finixpnum  37606  poimirlem3  37624  poimirlem4  37625  poimirlem8  37629  poimirlem26  37647  poimirlem27  37648  itg2gt0cn  37676  areacirclem2  37710  areacirclem4  37712  sdclem2  37743  caures  37761  ismtyres  37809  diaintclN  41059  dibintclN  41168  dihintcl  41345  fsuppssindlem1  42586  imaiinfv  42688  mzpcompact2lem  42746  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  jm2.27dlem1  43005  fnwe2lem2  43047  aomclem6  43055  deg1mhm  43196  hausgraph  43201  radcnvrat  44310  wessf1ornlem  45186  feqresmptf  45232  mccllem  45602  limcleqr  45649  limsupvaluz2  45743  supcnvlimsup  45745  limsupgtlem  45782  xlimconst2  45840  resincncf  45880  cncfperiod  45884  icccncfext  45892  cncfiooicclem1  45898  dvbdfbdioolem1  45933  dvnprodlem1  45951  dvnprodlem2  45952  itgioocnicc  45982  stoweidlem28  46033  fourierdlem18  46130  fourierdlem40  46152  fourierdlem42  46154  fourierdlem46  46157  fourierdlem51  46162  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem80  46191  fourierdlem81  46192  fourierdlem82  46193  fourierdlem84  46195  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem92  46203  fourierdlem93  46204  fourierdlem94  46205  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  sge0tsms  46385  sge0f1o  46387  sge0sup  46396  sge0less  46397  sge0ltfirp  46405  sge0resrnlem  46408  sge0resplit  46411  sge0le  46412  sge0split  46414  sge0fodjrnlem  46421  sge0iun  46424  meadjun  46467  meadjiunlem  46470  psmeasurelem  46475  caratheodory  46533  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  voncmpl  46626  mblvon  46644  smflimsuplem3  46827  afvres  47177  iccpartres  47423  iccelpart  47438  isubgredg  47870  isubgrgrim  47933  uhgrimisgrgric  47935  lincdifsn  48417  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  lincresunit3lem2  48473  fdivmpt  48533  slotresfo  48891  basresposfo  48970  oppff1  49141  setrec2lem1  49686  setrecsres  49695  amgmwlem  49795