Theorem fvres 6925

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 3481	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 6008	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6546	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6570	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6570	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2799	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   class class class wbr 5147   ↾ cres 5690  ℩cio 6513  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-res 5700  df-iota 6515  df-fv 6570

This theorem is referenced by:  fvresd  6926  funssfv  6927  fveqres  6953  feqresmpt  6977  dffv2  7003  eqfnun  7056  fvreseq0  7057  respreima  7085  fveqressseq  7098  ffvresb  7144  fnressn  7177  fressnfv  7179  fvresi  7192  funfvima  7249  funiunfv  7267  soisores  7346  isores3  7354  isoini2  7358  fvresval  7377  ofres  7715  f1oweALT  7995  offres  8006  fo1stres  8038  fo2ndres  8039  fparlem1  8135  fparlem2  8136  fsplitfpar  8141  fo2ndf  8144  f1o2ndf1  8145  fnsuppres  8214  wfrlem4OLD  8350  tfrlem1  8414  fr0g  8474  frsuc  8475  tz7.48lem  8479  seqomlem1  8488  seqomlem2  8489  seqomlem3  8490  seqomlem4  8491  onasuc  8564  onmsuc  8565  onesuc  8566  resixp  8971  fofinf1o  9369  ixpfi2  9387  ttrclss  9757  updjudhcoinlf  9969  updjudhcoinrg  9970  updjud  9971  ackbij2lem2  10276  ackbij2lem3  10277  cfsmolem  10307  alephsing  10313  fpwwe2lem7  10674  inar1  10812  addpiord  10921  mulpiord  10922  fseq1p1m1  13634  injresinj  13823  seqfeq2  14062  seqres  14066  seqf1olem2  14079  hashgval  14368  hashinf  14370  hashgval2  14413  hashf1lem1  14490  pfxccat1  14736  shftidt  15117  climres  15607  fsumss  15757  isumclim3  15791  fsum2dlem  15802  ackbijnn  15860  fprodss  15980  fprod2dlem  16012  iprodclim3  16032  bpolylem  16080  fprodefsum  16127  reeff1  16152  bitsf1  16479  sadcadd  16491  sadadd2  16493  eucalgcvga  16619  eucalg  16620  unbenlem  16941  strfv2d  17235  setsid  17241  setsnid  17242  setsnidOLD  17243  dfinito3  18058  dftermo3  18059  dmaf  18102  cdaf  18103  1stfcl  18252  2ndfcl  18253  resmgmhm  18736  resmhm  18845  resghm  19262  efgredlem  19779  gsumzaddlem  19953  dprdfadd  20054  dprdres  20062  dmdprdsplitlem  20071  dprdcntz2  20072  dmdprdsplit2lem  20079  dprdsplit  20082  dpjidcl  20092  ablfac1eu  20107  rngmgpf  20174  mgpf  20265  prdscrngd  20335  abvres  20848  reslmhm  21068  znf1o  21587  znunithash  21600  ltbwe  22079  subrgascl  22107  subrgasclcl  22108  smadiadetlem3  22689  lmres  23323  tx1cn  23632  tx2cn  23633  ptrescn  23662  cnmpt1st  23691  cnmpt2nd  23692  ptuncnv  23830  ptunhmeo  23831  cnextfres1  24091  prdstmdd  24147  prdsxmslem2  24557  subgnm2  24662  rescncf  24936  isncvsngp  25196  lmle  25348  ovoliunlem1  25550  ovolicc2lem4  25568  mblvol  25578  mbflimsup  25714  limcdif  25925  limcres  25935  dvres2lem  25959  dvlip  26046  dvlipcn  26047  dvlip2  26048  c1liplem1  26049  c1lip1  26050  c1lip3  26052  dvivthlem1  26061  lhop1lem  26066  lhop  26069  dvcvx  26073  ftc2ditglem  26100  itgsubstlem  26103  plyreres  26338  plyexmo  26369  aannenlem1  26384  taylthlem2  26430  taylthlem2OLD  26431  ulmres  26445  ulmss  26454  pserdvlem2  26486  reeff1o  26505  reefiso  26506  reefgim  26508  recosf1o  26591  resinf1o  26592  relogcl  26631  logef  26637  logeftb  26639  logltb  26656  logcn  26703  advlog  26710  advlogexp  26711  logtayl  26716  logccv  26719  dvcxp1  26796  dvcncxp1  26799  cxpcn  26801  cxpcnOLD  26802  loglesqrt  26818  dvatan  26992  leibpi  26999  efrlim  27026  efrlimOLD  27027  amgmlem  27047  lgamgulmlem2  27087  lgamcvg2  27112  wilthlem3  27127  ftalem3  27132  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  dchrelbas2  27295  dchrabs  27318  dchrisumlem1  27547  logdivsum  27591  log2sumbnd  27602  ostth2  27695  ostth  27697  sltres  27721  nodense  27751  nolt02o  27754  nogt01o  27755  noetainflem4  27799  vtxdginducedm1lem3  29573  redwlk  29704  pthdivtx  29761  pthdlem1  29798  ex-fpar  30490  sspnval  30765  hhssnv  31292  hhssmetdval  31305  foresf1o  32531  1stpreimas  32720  xpinpreima  33866  xpinpreima2  33867  cnre2csqlem  33870  zzsnm  33919  cnzh  33930  rezh  33931  measres  34202  cntmeas  34206  cntnevol  34208  1stmbfm  34241  2ndmbfm  34242  carsggect  34299  omsmeas  34304  eulerpartgbij  34353  eulerpartlemgvv  34357  eulerpartlemgs2  34361  iwrdsplit  34368  fibp1  34382  coinfliplem  34459  coinflipprob  34460  gsumnunsn  34534  plyrecld  34542  signstres  34568  ftc2re  34591  bnj1253  35009  bnj1280  35012  f1resveqaeq  35077  gblacfnacd  35091  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem8  35182  txsconnlem  35224  cvmfolem  35263  cvmliftmolem1  35265  cvmliftlem6  35274  cvmliftlem7  35275  cvmliftlem9  35277  satfsucom  35338  satom  35340  satfvsucom  35341  satf0sucom  35357  mrsubff1  35498  msubff1  35540  dfrdg2  35776  funpartfv  35926  filnetlem4  36363  icoreunrn  37341  finixpnum  37591  poimirlem3  37609  poimirlem4  37610  poimirlem8  37614  poimirlem26  37632  poimirlem27  37633  itg2gt0cn  37661  areacirclem2  37695  areacirclem4  37697  sdclem2  37728  caures  37746  ismtyres  37794  diaintclN  41040  dibintclN  41149  dihintcl  41326  fsuppssindlem1  42577  imaiinfv  42680  mzpcompact2lem  42738  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  jm2.27dlem1  42997  fnwe2lem2  43039  aomclem6  43047  deg1mhm  43188  hausgraph  43193  radcnvrat  44309  wessf1ornlem  45127  feqresmptf  45173  mccllem  45552  limcleqr  45599  limsupvaluz2  45693  supcnvlimsup  45695  limsupgtlem  45732  xlimconst2  45790  resincncf  45830  cncfperiod  45834  icccncfext  45842  cncfiooicclem1  45848  dvbdfbdioolem1  45883  dvnprodlem1  45901  dvnprodlem2  45902  itgioocnicc  45932  stoweidlem28  45983  fourierdlem18  46080  fourierdlem40  46102  fourierdlem42  46104  fourierdlem46  46107  fourierdlem51  46112  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem80  46141  fourierdlem81  46142  fourierdlem82  46143  fourierdlem84  46145  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem94  46155  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  sge0tsms  46335  sge0f1o  46337  sge0sup  46346  sge0less  46347  sge0ltfirp  46355  sge0resrnlem  46358  sge0resplit  46361  sge0le  46362  sge0split  46364  sge0fodjrnlem  46371  sge0iun  46374  meadjun  46417  meadjiunlem  46420  psmeasurelem  46425  caratheodory  46483  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  voncmpl  46576  mblvon  46594  smflimsuplem3  46777  afvres  47121  iccpartres  47342  iccelpart  47357  isubgredg  47789  isubgrgrim  47834  uhgrimisgrgric  47836  lincdifsn  48269  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  lincresunit3lem2  48325  fdivmpt  48389  setrec2lem1  48923  setrecsres  48932  amgmwlem  49032