Theorem reseq2d 5880

Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq2d	⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Proof of Theorem reseq2d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq2 5875	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890  df-opab 5133  df-xp 5586  df-res 5592

This theorem is referenced by:  reseq12d  5881  resresdm  6125  relresfld  6168  f1orescnv  6715  fococnv2  6725  fvn0ssdmfun  6934  fnressn  7012  fnsnsplit  7038  oprssov  7419  curry1  7915  curry2  7918  dftpos2  8030  frecseq123  8069  fpr3g  8072  frrlem1  8073  frrlem4  8076  frrlem12  8084  fpr2a  8089  wrecseq123OLD  8102  wfr3g  8109  wfrlem1OLD  8110  wfrlem4OLD  8114  wfrlem14OLD  8124  wfr2aOLD  8128  dfrecs3  8174  dfrecs3OLD  8175  tfrlem16  8195  tfr2ALT  8203  tfr3ALT  8204  sbthlem4  8826  mapunen  8882  hartogslem1  9231  frr3g  9445  frr2  9449  axdc3lem2  10138  fseq1p1m1  13259  resunimafz0  14085  hashf1lem1  14096  hashf1lem1OLD  14097  relexp0g  14661  relexp0  14662  relexpsucnnr  14664  dfrtrcl2  14701  bpolylem  15686  setsval  16796  idfuval  17507  idfu2nd  17508  resf1st  17525  setcid  17717  catcisolem  17741  estrcid  17766  funcestrcsetclem5  17777  funcsetcestrclem5  17792  funcsetcestrclem7  17794  1stfval  17824  1stf2  17826  2ndfval  17827  2ndf2  17829  1stfcl  17830  2ndfcl  17831  curf2ndf  17881  hofcl  17893  isps  18201  cnvps  18211  isdir  18231  dirref  18234  tsrdir  18237  frmdval  18405  frmdplusg  18408  gsum2dlem2  19487  dprd2da  19560  dpjval  19574  ablfac1eulem  19590  ablfac1eu  19591  psrplusg  21060  opsrtoslem2  21173  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  imacmp  22456  ptuncnv  22866  tgphaus  23176  tsmsres  23203  tsmsxplem1  23212  tsmsxplem2  23213  trust  23289  metreslem  23423  imasdsf1olem  23434  xmspropd  23534  mspropd  23535  imasf1oxms  23551  imasf1oms  23552  nmpropd2  23657  isngp2  23659  ngppropd  23699  tngngp2  23722  cphsscph  24320  cmspropd  24418  cmssmscld  24419  mbfres2  24714  limciun  24963  dvmptres3  25025  dvmptres2  25031  dvmptntr  25040  dvlipcn  25063  dvlip2  25064  c1liplem1  25065  dvgt0lem1  25071  lhop1lem  25082  dvcnvrelem1  25086  dvcvx  25089  ftc2ditglem  25114  wilthlem2  26123  dchrval  26287  dchrelbas2  26290  egrsubgr  27547  pthdlem1  28035  eupthvdres  28500  eupth2lem3  28501  eupth2  28504  eucrct2eupth  28510  hhssablo  29526  hhssnvt  29528  hhsssh  29532  fnunres1  30846  fressupp  30924  resf1o  30967  gsummpt2d  31211  gsumpart  31217  symgcom  31254  tocycval  31277  tocycfv  31278  tocycf  31286  tocyc01  31287  cycpm2tr  31288  cycpmconjslem1  31323  cycpmconjslem2  31324  nsgqusf1o  31503  qtophaus  31688  esumcvg  31954  eulerpartlemn  32248  sseqp1  32262  signsvtn0  32449  ftc2re  32478  reprsuc  32495  bnj1385  32712  bnj1326  32906  bnj1321  32907  bnj1442  32929  bnj1450  32930  bnj1463  32935  bnj1529  32950  f1resfz0f1d  32972  pfxwlk  32985  pthhashvtx  32989  cvmliftlem5  33151  cvmliftlem7  33153  cvmliftlem10  33156  cvmliftlem11  33157  cvmliftlem15  33160  cvmlift2lem11  33175  cvmlift2lem12  33176  satffunlem1lem1  33264  satffunlem2lem1  33266  eldm3  33634  funsseq  33648  on2recsov  33754  noresle  33827  nosupcbv  33832  nosupno  33833  nosupdm  33834  nosupfv  33836  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd1  33844  nosupbnd2  33846  noinfcbv  33847  noinfno  33848  noinfdm  33849  noinffv  33851  noinfres  33852  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd1  33859  noinfbnd2  33861  noetalem1  33871  norecov  34031  norec2ov  34041  finixpnum  35689  poimirlem3  35707  poimirlem4  35708  poimirlem9  35713  sdclem2  35827  prdsbnd2  35880  isdivrngo  36035  drngoi  36036  elrefsymrels2  36610  eleqvrels2  36632  dibffval  39081  hdmapffval  39767  hdmapfval  39768  eldiophb  40495  diophrw  40497  diophin  40510  rclexi  41112  rtrclex  41114  rtrclexi  41118  cnvrcl0  41122  dfrtrcl5  41126  dfrcl2  41171  fvmptiunrelexplb0da  41182  sblpnf  41817  fresin2  42597  limsupresuz  43134  limsupvaluz  43139  limsupvaluz2  43169  supcnvlimsup  43171  climrescn  43179  liminfresuz  43215  cncfuni  43317  dvresntr  43349  dvbdfbdioolem1  43359  itgiccshift  43411  itgperiod  43412  dirkercncflem2  43535  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem58  43595  fourierdlem72  43609  fourierdlem74  43611  fourierdlem75  43612  fourierdlem81  43618  fourierdlem88  43625  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fouriersw  43662  voncmpl  44049  funcoressn  44423  funressnmo  44427  f1cof1blem  44455  funfocofob  44457  funressndmafv2rn  44602  f1oresf1orab  44668  isomgreqve  45165  idfusubc0  45311  idfusubc  45312  rngcval  45408  rnghmsubcsetclem1  45421  rngccat  45424  rngcid  45425  rngcidALTV  45437  rngcifuestrc  45443  funcrngcsetc  45444  funcrngcsetcALT  45445  ringcval  45454  rhmsubcsetclem1  45467  ringccat  45470  ringcid  45471  rhmsubcrngclem1  45473  rhmsubcrngc  45475  funcringcsetc  45481  funcringcsetcALTV2lem5  45486  ringcidALTV  45500  funcringcsetclem5ALTV  45509  rhmsubc  45536  rhmsubcALTVlem3  45552  itcoval  45895  itcoval0mpt  45900  itcovalendof  45903  aacllem  46391