Theorem fvres 6207

Description: The value of a restricted function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fvres	|- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Proof of Theorem fvres

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3203	. . . . 5 |- x e. _V
2	1	brres 5402	. . . 4 |- ( A ( F |` B ) x <-> ( A F x /\ A e. B ) )
3	2	rbaib 947	. . 3 |- ( A e. B -> ( A ( F |` B ) x <-> A F x ) )
4	3	iotabidv 5872	. 2 |- ( A e. B -> ( iota x A ( F |` B ) x ) = ( iota x A F x ) )
5		df-fv 5896	. 2 |- ( ( F |` B ) ` A ) = ( iota x A ( F |` B ) x )
6		df-fv 5896	. 2 |- ( F ` A ) = ( iota x A F x )
7	4, 5, 6	3eqtr4g 2681	1 |- ( A e. B -> ( ( F |` B ) ` A ) = ( F ` A ) )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   class class class wbr 4653   |` cres 5116   iotacio 5849   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-res 5126  df-iota 5851  df-fv 5896

This theorem is referenced by:  fvresd  6208  funssfv  6209  fveqres  6230  feqresmpt  6250  dffv2  6271  fvreseq0  6317  respreima  6344  fveqressseq  6355  ffvresb  6394  fnressn  6425  fressnfv  6427  fvressn  6429  fvresi  6439  fvsnun1  6448  fvsnun2  6449  fsnunfv  6453  funfvima  6492  resfvresima  6494  funiunfv  6506  soisores  6577  isores3  6585  isoini2  6589  ovres  6800  ofres  6913  f1oweALT  7152  offres  7163  fo1stres  7192  fo2ndres  7193  curry1  7269  curry2  7272  fparlem1  7277  fparlem2  7278  fo2ndf  7284  f1o2ndf1  7285  fnsuppres  7322  wfrlem4  7418  smores  7449  smores2  7451  tfrlem1  7472  tz7.44-2  7503  fr0g  7531  frsuc  7532  tz7.48lem  7536  seqomlem1  7545  seqomlem2  7546  seqomlem3  7547  seqomlem4  7548  onasuc  7608  onmsuc  7609  onesuc  7610  resixp  7943  fofinf1o  8241  ixpfi2  8264  ordtypelem4  8426  ordtypelem6  8428  ordtypelem7  8429  unxpwdom2  8493  cantnfres  8574  cantnfp1lem3  8577  dfac12lem1  8965  ackbij2lem2  9062  ackbij2lem3  9063  cfsmolem  9092  alephsing  9098  ttukeylem3  9333  fpwwe2lem6  9457  fpwwe2lem8  9459  fpwwe2lem9  9460  canthp1lem2  9475  inar1  9597  addpiord  9706  mulpiord  9707  addpqnq  9760  mulpqnq  9763  fseq1p1m1  12414  injresinj  12589  seqfeq2  12824  seqres  12828  seqf1olem2  12841  hashgval  13120  hashinf  13122  hashgval2  13167  hashf1lem1  13239  seqcoll  13248  swrdccat1  13457  shftidt  13822  rlimres  14289  lo1res  14290  climres  14306  isercolllem3  14397  fsumss  14456  isumclim3  14490  fsum2dlem  14501  ackbijnn  14560  fprodss  14678  fprod2dlem  14710  iprodclim3  14731  bpolylem  14779  fprodefsum  14825  reeff1  14850  bitsf1  15168  sadcaddlem  15179  sadcadd  15180  sadadd2  15182  sadaddlem  15188  sadasslem  15192  sadeq  15194  eucalgcvga  15299  eucalg  15300  unbenlem  15612  strfv2d  15905  setsid  15914  setsnid  15915  funcres  16556  dmaf  16699  cdaf  16700  1stf1  16832  2ndf1  16835  1stfcl  16837  2ndfcl  16838  prf1st  16844  prf2nd  16845  1st2ndprf  16846  uncf2  16877  diag12  16884  diag2  16885  curf2ndf  16887  yonedalem22  16918  lubval  16984  glbval  16997  resmhm  17359  resghm  17676  efgsres  18151  efgredlemd  18157  efgredlem  18160  gsumzaddlem  18321  dprdfadd  18419  dprdres  18427  dmdprdsplitlem  18436  dprdcntz2  18437  dmdprdsplit2lem  18444  dprdsplit  18447  dpjidcl  18457  ablfac1eu  18472  mgpf  18559  prdscrngd  18613  abvres  18839  reslmhm  19052  ltbwe  19472  subrgascl  19498  subrgasclcl  19499  znf1o  19900  znunithash  19913  psgndiflemB  19946  smadiadetlem3  20474  cnpresti  21092  cnprest  21093  lmres  21104  tx1cn  21412  tx2cn  21413  upxp  21426  uptx  21428  ptrescn  21442  cnmpt1st  21471  cnmpt2nd  21472  ptuncnv  21610  ptunhmeo  21611  cnextfres1  21872  prdstmdd  21927  prdsxmslem2  22334  subgnm2  22438  remetdval  22592  rescncf  22700  isncvsngp  22949  lmle  23099  lmcau  23111  ovoliunlem1  23270  ovolicc2lem4  23288  mblvol  23298  mbflimsup  23433  limcdif  23640  limcres  23650  dvreslem  23673  dvres2lem  23674  dvlip  23756  dvlipcn  23757  dvlip2  23758  c1liplem1  23759  c1lip1  23760  c1lip3  23762  dvgt0lem1  23765  dvivthlem1  23771  lhop1lem  23776  lhop  23779  dvcnvrelem1  23780  dvcvx  23783  ftc2ditglem  23808  itgsubstlem  23811  plyreres  24038  plyexmo  24068  aannenlem1  24083  taylthlem2  24128  ulmres  24142  ulmss  24151  psercn  24180  pserdvlem2  24182  reeff1o  24201  reefiso  24202  efcvx  24203  reefgim  24204  recosf1o  24281  resinf1o  24282  efif1olem4  24291  eff1olem  24294  relogcl  24322  eflog  24323  logef  24328  logeftb  24330  logltb  24346  logcn  24393  advlog  24400  advlogexp  24401  logtayl  24406  logccv  24409  dvcxp1  24481  dvcncxp1  24484  cxpcn  24486  loglesqrt  24499  asinrebnd  24628  dvatan  24662  leibpi  24669  efrlim  24696  jensen  24715  amgmlem  24716  lgamgulmlem2  24756  lgamcvg2  24781  wilthlem3  24796  ftalem3  24801  dvdsmulf1o  24920  fsumdvdsmul  24921  dchrelbas2  24962  dchrabs  24985  sum2dchr  24999  dchrisumlem1  25178  logdivsum  25222  log2sumbnd  25233  ostth2  25326  ostth  25328  vtxdginducedm1lem3  26437  wlkres  26567  redwlk  26569  pthdivtx  26625  pthdlem1  26662  sspnval  27592  hhssnv  28121  hhssmetdval  28135  foresf1o  29343  ofresid  29444  1stpreimas  29483  xpinpreima  29952  xpinpreima2  29953  cnre2csqlem  29956  rmulccn  29974  zzsnm  30005  cnzh  30014  rezh  30015  measres  30285  cntmeas  30289  cntnevol  30291  1stmbfm  30322  2ndmbfm  30323  carsggect  30380  omsmeas  30385  eulerpartgbij  30434  eulerpartlemgvv  30438  eulerpartlemgs2  30442  iwrdsplit  30449  fibp1  30463  coinfliplem  30540  coinflipprob  30541  gsumnunsn  30615  plyrecld  30626  signstres  30652  ftc2re  30676  bnj1379  30901  bnj1253  31085  bnj1280  31088  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem8  31180  txsconnlem  31222  cvmfolem  31261  cvmliftmolem1  31263  cvmliftlem6  31272  cvmliftlem7  31273  cvmliftlem9  31275  mrsubff1  31411  msubff1  31453  fvresval  31665  dfrdg2  31701  frrlem4  31783  sltres  31815  nodense  31842  nolt02o  31845  funpartfv  32052  filnetlem4  32376  icoreunrn  33207  finixpnum  33394  poimirlem3  33412  poimirlem4  33413  poimirlem8  33417  poimirlem26  33435  poimirlem27  33436  itg2gt0cn  33465  areacirclem2  33501  areacirclem4  33503  eqfnun  33516  sdclem2  33538  caures  33556  ismtyres  33607  diaintclN  36347  dibintclN  36456  dihintcl  36633  imaiinfv  37256  mzpcompact2lem  37314  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  jm2.27dlem1  37576  fnwe2lem2  37621  fnwe2lem3  37622  aomclem6  37629  deg1mhm  37785  hausgraph  37790  radcnvrat  38513  wessf1ornlem  39371  feqresmptf  39433  mccllem  39829  limcperiod  39860  limcleqr  39876  limclner  39883  limsupvaluz2  39970  supcnvlimsup  39972  limsupgtlem  40009  xlimconst2  40061  resincncf  40088  cncfperiod  40092  icccncfext  40100  cncfiooicclem1  40106  dvbdfbdioolem1  40143  dvnprodlem1  40161  dvnprodlem2  40162  itgioocnicc  40193  stoweidlem28  40245  fourierdlem18  40342  fourierdlem40  40364  fourierdlem42  40366  fourierdlem46  40369  fourierdlem51  40374  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem80  40403  fourierdlem81  40404  fourierdlem82  40405  fourierdlem84  40407  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem94  40417  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  sge0tsms  40597  sge0f1o  40599  sge0sup  40608  sge0less  40609  sge0ltfirp  40617  sge0resrnlem  40620  sge0resplit  40623  sge0le  40624  sge0split  40626  sge0fodjrnlem  40633  sge0iun  40636  meadjun  40679  meadjiunlem  40682  psmeasurelem  40687  caratheodory  40742  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  voncmpl  40835  mblvon  40853  smflimsuplem3  41028  afvres  41252  iccpartres  41354  iccelpart  41369  pfxccat1  41410  resmgmhm  41798  rhmsubclem2  42087  rhmsubcALTVlem2  42105  lincdifsn  42213  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  lincresunit3lem2  42269  fdivmpt  42334  setrec2lem1  42440  amgmwlem  42548