Theorem fvres 6900

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 3459	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5987	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 544	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6520	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6544	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6544	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2823	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   class class class wbr 5109   ↾ cres 5663  ℩cio 6490  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-res 5673  df-iota 6492  df-fv 6544

This theorem is referenced by:  fvresd  6901  funssfv  6902  fveqres  6925  feqresmpt  6950  dffv2  6976  eqfnun  7032  fvreseq0  7033  respreima  7061  fveqressseq  7074  ffvresb  7121  fnressn  7155  fressnfv  7157  fvresi  7171  funfvima  7228  funiunfv  7246  soisores  7325  isores3  7333  isoini2  7337  fvresval  7356  ofres  7693  f1oweALT  7965  offres  7976  fo1stres  8008  fo2ndres  8009  fparlem1  8103  fparlem2  8104  fsplitfpar  8109  fo2ndf  8112  f1o2ndf1  8113  fnsuppres  8183  tfrlem1  8358  fr0g  8419  frsuc  8420  tz7.48lem  8424  seqomlem1  8433  seqomlem2  8434  seqomlem3  8435  seqomlem4  8436  onasuc  8509  onmsuc  8510  onesuc  8511  resixp  8927  fofinf1o  9285  ixpfi2  9303  ttrclss  9685  updjudhcoinlf  9914  updjudhcoinrg  9915  updjud  9916  ackbij2lem2  10218  ackbij2lem3  10219  cfsmolem  10249  alephsing  10255  fpwwe2lem7  10617  inar1  10755  addpiord  10864  mulpiord  10865  fseq1p1m1  13622  injresinj  13816  seqfeq2  14057  seqres  14061  seqf1olem2  14074  hashgval  14365  hashinf  14367  hashgval2  14410  hashf1lem1  14488  pfxccat1  14735  shftidt  15115  climres  15622  fsumss  15772  isumclim3  15806  fsum2dlem  15817  ackbijnn  15878  fprodss  15998  fprod2dlem  16030  iprodclim3  16050  bpolylem  16097  fprodefsum  16144  reeff1  16171  bitsf1  16499  sadcadd  16511  sadadd2  16513  eucalgcvga  16639  eucalg  16640  unbenlem  16963  strfv2d  17256  setsid  17262  setsnid  17263  dfinito3  18057  dftermo3  18058  dmaf  18101  cdaf  18102  1stfcl  18248  2ndfcl  18249  resmgmhm  18764  resmhm  18874  resghm  19297  efgredlem  19812  gsumzaddlem  19986  dprdfadd  20087  dprdres  20095  dmdprdsplitlem  20104  dprdcntz2  20105  dmdprdsplit2lem  20112  dprdsplit  20115  dpjidcl  20125  ablfac1eu  20140  rngmgpf  20230  mgpf  20325  prdscrngd  20399  abvres  20934  reslmhm  21173  znf1o  21701  znunithash  21714  ltbwe  22195  subrgascl  22217  subrgasclcl  22218  smadiadetlem3  22825  lmres  23457  tx1cn  23766  tx2cn  23767  ptrescn  23796  cnmpt1st  23825  cnmpt2nd  23826  ptuncnv  23964  ptunhmeo  23965  cnextfres1  24225  prdstmdd  24281  prdsxmslem2  24686  subgnm2  24791  rescncf  25056  isncvsngp  25308  lmle  25460  ovoliunlem1  25661  ovolicc2lem4  25679  mblvol  25689  mbflimsup  25825  limcdif  26035  limcres  26045  dvres2lem  26069  dvlip  26152  dvlipcn  26153  dvlip2  26154  c1liplem1  26155  c1lip1  26156  c1lip3  26158  dvivthlem1  26167  lhop1lem  26172  lhop  26175  dvcvx  26179  ftc2ditglem  26204  itgsubstlem  26207  plyreres  26444  plyexmo  26474  aannenlem1  26491  taylthlem2  26537  ulmres  26551  ulmss  26560  pserdvlem2  26591  reeff1o  26610  reefiso  26611  reefgim  26613  recosf1o  26700  resinf1o  26701  relogcl  26740  logef  26746  logeftb  26748  logltb  26765  logcn  26812  advlog  26819  advlogexp  26820  logtayl  26825  logccv  26828  dvcxp1  26905  dvcncxp1  26908  cxpcn  26910  loglesqrt  26926  dvatan  27100  leibpi  27107  efrlim  27134  amgmlem  27154  lgamgulmlem2  27194  lgamcvg2  27219  wilthlem3  27234  ftalem3  27239  mpodvdsmulf1o  27358  fsumdvdsmul  27359  dvdsmulf1o  27360  dchrelbas2  27401  dchrabs  27424  dchrisumlem1  27653  logdivsum  27697  log2sumbnd  27708  ostth2  27801  ostth  27803  ltsres  27826  nodense  27856  nolt02o  27859  nogt01o  27860  noetainflem4  27904  oniso  28464  bdayn0sf1o  28563  vtxdginducedm1lem3  29891  redwlk  30020  pthdivtx  30076  pthdlem1  30115  ex-fpar  30813  sspnval  31089  hhssnv  31616  hhssmetdval  31629  foresf1o  32850  1stpreimas  33051  cos9thpiminply  34178  xpinpreima  34296  xpinpreima2  34297  cnre2csqlem  34300  zzsnm  34349  cnzh  34358  rezh  34359  measres  34612  cntmeas  34616  cntnevol  34618  1stmbfm  34650  2ndmbfm  34651  carsggect  34708  omsmeas  34713  eulerpartgbij  34762  eulerpartlemgvv  34766  eulerpartlemgs2  34770  iwrdsplit  34777  fibp1  34791  coinfliplem  34869  coinflipprob  34870  gsumnunsn  34931  plyrecld  34936  signstres  34962  ftc2re  34985  bnj1253  35405  bnj1280  35408  f1resveqaeq  35473  noinfepregs  35546  gblacfnacd  35586  subfacp1lem3  35674  subfacp1lem5  35676  erdszelem8  35690  txsconnlem  35732  cvmfolem  35771  cvmliftmolem1  35773  cvmliftlem6  35782  cvmliftlem7  35783  cvmliftlem9  35785  satfsucom  35846  satom  35848  satfvsucom  35849  satf0sucom  35865  mrsubff1  36006  msubff1  36048  dfrdg2  36285  funpartfv  36437  filnetlem4  36892  icoreunrn  38005  finixpnum  38256  poimirlem3  38274  poimirlem4  38275  poimirlem8  38279  poimirlem26  38297  poimirlem27  38298  itg2gt0cn  38326  areacirclem2  38360  areacirclem4  38362  sdclem2  38393  caures  38411  ismtyres  38459  diaintclN  41832  dibintclN  41941  dihintcl  42118  fsuppssindlem1  43323  imaiinfv  43424  mzpcompact2lem  43482  2rexfrabdioph  43523  3rexfrabdioph  43524  4rexfrabdioph  43525  6rexfrabdioph  43526  7rexfrabdioph  43527  jm2.27dlem1  43736  fnwe2lem2  43778  aomclem6  43786  deg1mhm  43927  hausgraph  43932  radcnvrat  45024  hashnna  45728  hashomiso  45734  wessf1ornlem  45903  feqresmptf  45946  mccllem  46313  limcleqr  46358  limsupvaluz2  46452  supcnvlimsup  46454  limsupgtlem  46491  xlimconst2  46549  resincncf  46589  cncfperiod  46593  icccncfext  46601  cncfiooicclem1  46607  dvbdfbdioolem1  46642  dvnprodlem1  46660  dvnprodlem2  46661  itgioocnicc  46691  stoweidlem28  46742  fourierdlem18  46839  fourierdlem40  46861  fourierdlem42  46863  fourierdlem46  46866  fourierdlem51  46871  fourierdlem70  46890  fourierdlem71  46891  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem78  46898  fourierdlem80  46900  fourierdlem81  46901  fourierdlem82  46902  fourierdlem84  46904  fourierdlem89  46909  fourierdlem90  46910  fourierdlem91  46911  fourierdlem92  46912  fourierdlem93  46913  fourierdlem94  46914  fourierdlem101  46921  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fourierdlem112  46932  fourierdlem113  46933  sge0tsms  47094  sge0f1o  47096  sge0sup  47105  sge0less  47106  sge0ltfirp  47114  sge0resrnlem  47117  sge0resplit  47120  sge0le  47121  sge0split  47123  sge0fodjrnlem  47130  sge0iun  47133  meadjun  47176  meadjiunlem  47179  psmeasurelem  47184  caratheodory  47242  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvlelem4  47312  voncmpl  47335  mblvon  47353  smflimsuplem3  47536  cjnpoly  47626  afvres  47909  iccpartres  48167  iccelpart  48182  isubgredg  48631  isubgrgrim  48694  uhgrimisgrgric  48696  lincdifsn  49204  lindslinindimp2lem4  49241  lindslinindsimp2lem5  49242  lincresunit3lem2  49260  fdivmpt  49320  slotresfo  49677  basresposfo  49756  oppff1  49926  setrec2lem1  50471  setrecsres  50480  amgmwlem  50622