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 3484	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 6006	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 535	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6545	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6569	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6569	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2802	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   class class class wbr 5143   ↾ cres 5687  ℩cio 6512  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-res 5697  df-iota 6514  df-fv 6569

This theorem is referenced by:  fvresd  6926  funssfv  6927  fveqres  6953  feqresmpt  6978  dffv2  7004  eqfnun  7057  fvreseq0  7058  respreima  7086  fveqressseq  7099  ffvresb  7145  fnressn  7178  fressnfv  7180  fvresi  7193  funfvima  7250  funiunfv  7268  soisores  7347  isores3  7355  isoini2  7359  fvresval  7378  ofres  7716  f1oweALT  7997  offres  8008  fo1stres  8040  fo2ndres  8041  fparlem1  8137  fparlem2  8138  fsplitfpar  8143  fo2ndf  8146  f1o2ndf1  8147  fnsuppres  8216  wfrlem4OLD  8352  tfrlem1  8416  fr0g  8476  frsuc  8477  tz7.48lem  8481  seqomlem1  8490  seqomlem2  8491  seqomlem3  8492  seqomlem4  8493  onasuc  8566  onmsuc  8567  onesuc  8568  resixp  8973  fofinf1o  9372  ixpfi2  9390  ttrclss  9760  updjudhcoinlf  9972  updjudhcoinrg  9973  updjud  9974  ackbij2lem2  10279  ackbij2lem3  10280  cfsmolem  10310  alephsing  10316  fpwwe2lem7  10677  inar1  10815  addpiord  10924  mulpiord  10925  fseq1p1m1  13638  injresinj  13827  seqfeq2  14066  seqres  14070  seqf1olem2  14083  hashgval  14372  hashinf  14374  hashgval2  14417  hashf1lem1  14494  pfxccat1  14740  shftidt  15121  climres  15611  fsumss  15761  isumclim3  15795  fsum2dlem  15806  ackbijnn  15864  fprodss  15984  fprod2dlem  16016  iprodclim3  16036  bpolylem  16084  fprodefsum  16131  reeff1  16156  bitsf1  16483  sadcadd  16495  sadadd2  16497  eucalgcvga  16623  eucalg  16624  unbenlem  16946  strfv2d  17238  setsid  17244  setsnid  17245  setsnidOLD  17246  dfinito3  18050  dftermo3  18051  dmaf  18094  cdaf  18095  1stfcl  18242  2ndfcl  18243  resmgmhm  18724  resmhm  18833  resghm  19250  efgredlem  19765  gsumzaddlem  19939  dprdfadd  20040  dprdres  20048  dmdprdsplitlem  20057  dprdcntz2  20058  dmdprdsplit2lem  20065  dprdsplit  20068  dpjidcl  20078  ablfac1eu  20093  rngmgpf  20154  mgpf  20245  prdscrngd  20319  abvres  20832  reslmhm  21051  znf1o  21570  znunithash  21583  ltbwe  22062  subrgascl  22090  subrgasclcl  22091  smadiadetlem3  22674  lmres  23308  tx1cn  23617  tx2cn  23618  ptrescn  23647  cnmpt1st  23676  cnmpt2nd  23677  ptuncnv  23815  ptunhmeo  23816  cnextfres1  24076  prdstmdd  24132  prdsxmslem2  24542  subgnm2  24647  rescncf  24923  isncvsngp  25183  lmle  25335  ovoliunlem1  25537  ovolicc2lem4  25555  mblvol  25565  mbflimsup  25701  limcdif  25911  limcres  25921  dvres2lem  25945  dvlip  26032  dvlipcn  26033  dvlip2  26034  c1liplem1  26035  c1lip1  26036  c1lip3  26038  dvivthlem1  26047  lhop1lem  26052  lhop  26055  dvcvx  26059  ftc2ditglem  26086  itgsubstlem  26089  plyreres  26324  plyexmo  26355  aannenlem1  26370  taylthlem2  26416  taylthlem2OLD  26417  ulmres  26431  ulmss  26440  pserdvlem2  26472  reeff1o  26491  reefiso  26492  reefgim  26494  recosf1o  26577  resinf1o  26578  relogcl  26617  logef  26623  logeftb  26625  logltb  26642  logcn  26689  advlog  26696  advlogexp  26697  logtayl  26702  logccv  26705  dvcxp1  26782  dvcncxp1  26785  cxpcn  26787  cxpcnOLD  26788  loglesqrt  26804  dvatan  26978  leibpi  26985  efrlim  27012  efrlimOLD  27013  amgmlem  27033  lgamgulmlem2  27073  lgamcvg2  27098  wilthlem3  27113  ftalem3  27118  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  dchrelbas2  27281  dchrabs  27304  dchrisumlem1  27533  logdivsum  27577  log2sumbnd  27588  ostth2  27681  ostth  27683  sltres  27707  nodense  27737  nolt02o  27740  nogt01o  27741  noetainflem4  27785  vtxdginducedm1lem3  29559  redwlk  29690  pthdivtx  29747  pthdlem1  29786  ex-fpar  30481  sspnval  30756  hhssnv  31283  hhssmetdval  31296  foresf1o  32523  1stpreimas  32715  xpinpreima  33905  xpinpreima2  33906  cnre2csqlem  33909  zzsnm  33958  cnzh  33969  rezh  33970  measres  34223  cntmeas  34227  cntnevol  34229  1stmbfm  34262  2ndmbfm  34263  carsggect  34320  omsmeas  34325  eulerpartgbij  34374  eulerpartlemgvv  34378  eulerpartlemgs2  34382  iwrdsplit  34389  fibp1  34403  coinfliplem  34481  coinflipprob  34482  gsumnunsn  34556  plyrecld  34564  signstres  34590  ftc2re  34613  bnj1253  35031  bnj1280  35034  f1resveqaeq  35099  gblacfnacd  35113  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem8  35203  txsconnlem  35245  cvmfolem  35284  cvmliftmolem1  35286  cvmliftlem6  35295  cvmliftlem7  35296  cvmliftlem9  35298  satfsucom  35359  satom  35361  satfvsucom  35362  satf0sucom  35378  mrsubff1  35519  msubff1  35561  dfrdg2  35796  funpartfv  35946  filnetlem4  36382  icoreunrn  37360  finixpnum  37612  poimirlem3  37630  poimirlem4  37631  poimirlem8  37635  poimirlem26  37653  poimirlem27  37654  itg2gt0cn  37682  areacirclem2  37716  areacirclem4  37718  sdclem2  37749  caures  37767  ismtyres  37815  diaintclN  41060  dibintclN  41169  dihintcl  41346  fsuppssindlem1  42601  imaiinfv  42704  mzpcompact2lem  42762  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  jm2.27dlem1  43021  fnwe2lem2  43063  aomclem6  43071  deg1mhm  43212  hausgraph  43217  radcnvrat  44333  wessf1ornlem  45190  feqresmptf  45236  mccllem  45612  limcleqr  45659  limsupvaluz2  45753  supcnvlimsup  45755  limsupgtlem  45792  xlimconst2  45850  resincncf  45890  cncfperiod  45894  icccncfext  45902  cncfiooicclem1  45908  dvbdfbdioolem1  45943  dvnprodlem1  45961  dvnprodlem2  45962  itgioocnicc  45992  stoweidlem28  46043  fourierdlem18  46140  fourierdlem40  46162  fourierdlem42  46164  fourierdlem46  46167  fourierdlem51  46172  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem80  46201  fourierdlem81  46202  fourierdlem82  46203  fourierdlem84  46205  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem94  46215  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  sge0tsms  46395  sge0f1o  46397  sge0sup  46406  sge0less  46407  sge0ltfirp  46415  sge0resrnlem  46418  sge0resplit  46421  sge0le  46422  sge0split  46424  sge0fodjrnlem  46431  sge0iun  46434  meadjun  46477  meadjiunlem  46480  psmeasurelem  46485  caratheodory  46543  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  voncmpl  46636  mblvon  46654  smflimsuplem3  46837  afvres  47184  iccpartres  47405  iccelpart  47420  isubgredg  47852  isubgrgrim  47897  uhgrimisgrgric  47899  lincdifsn  48341  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  lincresunit3lem2  48397  fdivmpt  48461  setrec2lem1  49212  setrecsres  49221  amgmwlem  49321