Theorem fvres 6714

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 3402	. . . . 5 ⊢ 𝑥 ∈ V
2	1	brresi 5845	. . . 4 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ (𝐴 ∈ 𝐵 ∧ 𝐴𝐹𝑥))
3	2	baib 539	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ 𝐴𝐹𝑥))
4	3	iotabidv 6342	. 2 ⊢ (𝐴 ∈ 𝐵 → (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = (℩𝑥𝐴𝐹𝑥))
5		df-fv 6366	. 2 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
6		df-fv 6366	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
7	4, 5, 6	3eqtr4g 2796	1 ⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴))

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112   class class class wbr 5039   ↾ cres 5538  ℩cio 6314  ‘cfv 6358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-xp 5542  df-res 5548  df-iota 6316  df-fv 6366

This theorem is referenced by:  fvresd  6715  funssfv  6716  fveqres  6737  feqresmpt  6759  dffv2  6784  fvreseq0  6836  respreima  6864  fveqressseq  6878  ffvresb  6919  fnressn  6951  fressnfv  6953  fvresi  6966  funfvima  7024  funiunfv  7039  soisores  7114  isores3  7122  isoini2  7126  ofres  7465  f1oweALT  7723  offres  7734  fo1stres  7765  fo2ndres  7766  fparlem1  7858  fparlem2  7859  fsplitfpar  7865  fo2ndf  7868  f1o2ndf1  7869  fnsuppres  7911  wfrlem4  8036  tfrlem1  8090  fr0g  8149  frsuc  8150  tz7.48lem  8155  seqomlem1  8164  seqomlem2  8165  seqomlem3  8166  seqomlem4  8167  onasuc  8233  onmsuc  8234  onesuc  8235  resixp  8592  fofinf1o  8929  ixpfi2  8952  updjudhcoinlf  9513  updjudhcoinrg  9514  updjud  9515  ackbij2lem2  9819  ackbij2lem3  9820  cfsmolem  9849  alephsing  9855  fpwwe2lem7  10216  inar1  10354  addpiord  10463  mulpiord  10464  fseq1p1m1  13151  injresinj  13328  seqfeq2  13564  seqres  13568  seqf1olem2  13581  hashgval  13864  hashinf  13866  hashgval2  13910  hashf1lem1  13985  hashf1lem1OLD  13986  pfxccat1  14232  shftidt  14610  climres  15101  fsumss  15254  isumclim3  15286  fsum2dlem  15297  ackbijnn  15355  fprodss  15473  fprod2dlem  15505  iprodclim3  15525  bpolylem  15573  fprodefsum  15619  reeff1  15644  bitsf1  15968  sadcadd  15980  sadadd2  15982  eucalgcvga  16106  eucalg  16107  unbenlem  16424  strfv2d  16711  setsid  16719  setsnid  16720  dfinito3  17465  dftermo3  17466  dmaf  17509  cdaf  17510  1stfcl  17658  2ndfcl  17659  resmhm  18201  resghm  18592  efgredlem  19091  gsumzaddlem  19260  dprdfadd  19361  dprdres  19369  dmdprdsplitlem  19378  dprdcntz2  19379  dmdprdsplit2lem  19386  dprdsplit  19389  dpjidcl  19399  ablfac1eu  19414  mgpf  19531  prdscrngd  19585  abvres  19829  reslmhm  20043  znf1o  20470  znunithash  20483  ltbwe  20955  subrgascl  20978  subrgasclcl  20979  smadiadetlem3  21519  lmres  22151  tx1cn  22460  tx2cn  22461  ptrescn  22490  cnmpt1st  22519  cnmpt2nd  22520  ptuncnv  22658  ptunhmeo  22659  cnextfres1  22919  prdstmdd  22975  prdsxmslem2  23381  subgnm2  23486  rescncf  23748  isncvsngp  24000  lmle  24152  ovoliunlem1  24353  ovolicc2lem4  24371  mblvol  24381  mbflimsup  24517  limcdif  24727  limcres  24737  dvres2lem  24761  dvlip  24844  dvlipcn  24845  dvlip2  24846  c1liplem1  24847  c1lip1  24848  c1lip3  24850  dvivthlem1  24859  lhop1lem  24864  lhop  24867  dvcvx  24871  ftc2ditglem  24896  itgsubstlem  24899  plyreres  25130  plyexmo  25160  aannenlem1  25175  taylthlem2  25220  ulmres  25234  ulmss  25243  pserdvlem2  25274  reeff1o  25293  reefiso  25294  reefgim  25296  recosf1o  25378  resinf1o  25379  relogcl  25418  logef  25424  logeftb  25426  logltb  25442  logcn  25489  advlog  25496  advlogexp  25497  logtayl  25502  logccv  25505  dvcxp1  25580  dvcncxp1  25583  cxpcn  25585  loglesqrt  25598  dvatan  25772  leibpi  25779  efrlim  25806  amgmlem  25826  lgamgulmlem2  25866  lgamcvg2  25891  wilthlem3  25906  ftalem3  25911  dvdsmulf1o  26030  fsumdvdsmul  26031  dchrelbas2  26072  dchrabs  26095  dchrisumlem1  26324  logdivsum  26368  log2sumbnd  26379  ostth2  26472  ostth  26474  vtxdginducedm1lem3  27583  redwlk  27714  pthdivtx  27770  pthdlem1  27807  ex-fpar  28499  sspnval  28772  hhssnv  29299  hhssmetdval  29312  foresf1o  30523  1stpreimas  30712  xpinpreima  31524  xpinpreima2  31525  cnre2csqlem  31528  rmulccn  31546  zzsnm  31577  cnzh  31586  rezh  31587  measres  31856  cntmeas  31860  cntnevol  31862  1stmbfm  31893  2ndmbfm  31894  carsggect  31951  omsmeas  31956  eulerpartgbij  32005  eulerpartlemgvv  32009  eulerpartlemgs2  32013  iwrdsplit  32020  fibp1  32034  coinfliplem  32111  coinflipprob  32112  gsumnunsn  32186  plyrecld  32194  signstres  32220  ftc2re  32244  bnj1253  32664  bnj1280  32667  f1resveqaeq  32724  subfacp1lem3  32811  subfacp1lem5  32813  erdszelem8  32827  txsconnlem  32869  cvmfolem  32908  cvmliftmolem1  32910  cvmliftlem6  32919  cvmliftlem7  32920  cvmliftlem9  32922  satfsucom  32983  satom  32985  satfvsucom  32986  satf0sucom  33002  mrsubff1  33143  msubff1  33185  fvresval  33411  dfrdg2  33441  sltres  33551  nodense  33581  nolt02o  33584  nogt01o  33585  noetainflem4  33629  funpartfv  33933  filnetlem4  34256  icoreunrn  35216  finixpnum  35448  poimirlem3  35466  poimirlem4  35467  poimirlem8  35471  poimirlem26  35489  poimirlem27  35490  itg2gt0cn  35518  areacirclem2  35552  areacirclem4  35554  eqfnun  35566  sdclem2  35586  caures  35604  ismtyres  35652  diaintclN  38758  dibintclN  38867  dihintcl  39044  fsuppssindlem1  39931  imaiinfv  40159  mzpcompact2lem  40217  2rexfrabdioph  40262  3rexfrabdioph  40263  4rexfrabdioph  40264  6rexfrabdioph  40265  7rexfrabdioph  40266  jm2.27dlem1  40475  fnwe2lem2  40520  aomclem6  40528  deg1mhm  40676  hausgraph  40681  radcnvrat  41546  wessf1ornlem  42336  feqresmptf  42386  mccllem  42756  limcleqr  42803  limsupvaluz2  42897  supcnvlimsup  42899  limsupgtlem  42936  xlimconst2  42994  resincncf  43034  cncfperiod  43038  icccncfext  43046  cncfiooicclem1  43052  dvbdfbdioolem1  43087  dvnprodlem1  43105  dvnprodlem2  43106  itgioocnicc  43136  stoweidlem28  43187  fourierdlem18  43284  fourierdlem40  43306  fourierdlem42  43308  fourierdlem46  43311  fourierdlem51  43316  fourierdlem70  43335  fourierdlem71  43336  fourierdlem73  43338  fourierdlem74  43339  fourierdlem75  43340  fourierdlem76  43341  fourierdlem78  43343  fourierdlem80  43345  fourierdlem81  43346  fourierdlem82  43347  fourierdlem84  43349  fourierdlem89  43354  fourierdlem90  43355  fourierdlem91  43356  fourierdlem92  43357  fourierdlem93  43358  fourierdlem94  43359  fourierdlem101  43366  fourierdlem103  43368  fourierdlem104  43369  fourierdlem111  43376  fourierdlem112  43377  fourierdlem113  43378  sge0tsms  43536  sge0f1o  43538  sge0sup  43547  sge0less  43548  sge0ltfirp  43556  sge0resrnlem  43559  sge0resplit  43562  sge0le  43563  sge0split  43565  sge0fodjrnlem  43572  sge0iun  43575  meadjun  43618  meadjiunlem  43621  psmeasurelem  43626  caratheodory  43684  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  voncmpl  43777  mblvon  43795  smflimsuplem3  43970  afvres  44279  iccpartres  44486  iccelpart  44501  resmgmhm  44968  lincdifsn  45381  lindslinindimp2lem4  45418  lindslinindsimp2lem5  45419  lincresunit3lem2  45437  fdivmpt  45502  setrec2lem1  46013  setrecsres  46021  amgmwlem  46120