Theorem reseq2d 5834

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 5829	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1537   ↾ cres 5538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-rab 3142  df-in 3926  df-opab 5110  df-xp 5542  df-res 5548

This theorem is referenced by:  reseq12d  5835  resresdm  6071  relresfld  6108  f1orescnv  6611  fococnv2  6621  fvn0ssdmfun  6823  fnressn  6901  fnsnsplit  6927  oprssov  7298  curry1  7780  curry2  7783  dftpos2  7890  wrecseq123  7929  wfr3g  7934  wfrlem1  7935  wfrlem4  7939  wfrlem14  7949  wfr2a  7953  dfrecs3  7990  tfrlem16  8010  tfr2ALT  8018  tfr3ALT  8019  sbthlem4  8611  mapunen  8667  hartogslem1  8987  axdc3lem2  9854  fseq1p1m1  12966  resunimafz0  13788  hashf1lem1  13798  relexp0g  14361  relexp0  14362  relexpsucnnr  14364  dfrtrcl2  14401  bpolylem  15382  setsval  16491  idfuval  17124  idfu2nd  17125  resf1st  17142  setcid  17324  catcisolem  17344  estrcid  17362  funcestrcsetclem5  17372  funcsetcestrclem5  17387  funcsetcestrclem7  17389  1stfval  17419  1stf2  17421  2ndfval  17422  2ndf2  17424  1stfcl  17425  2ndfcl  17426  curf2ndf  17475  hofcl  17487  isps  17790  cnvps  17800  isdir  17820  dirref  17823  tsrdir  17826  frmdval  17994  frmdplusg  17997  gsum2dlem2  19069  dprd2da  19142  dpjval  19156  ablfac1eulem  19172  ablfac1eu  19173  psrplusg  20139  opsrtoslem2  20243  mdetunilem3  21201  mdetunilem4  21202  mdetunilem9  21207  imacmp  21983  ptuncnv  22393  tgphaus  22703  tsmsres  22730  tsmsxplem1  22739  tsmsxplem2  22740  trust  22816  metreslem  22950  imasdsf1olem  22961  xmspropd  23061  mspropd  23062  imasf1oxms  23077  imasf1oms  23078  nmpropd2  23182  isngp2  23184  ngppropd  23224  tngngp2  23239  cphsscph  23832  cmspropd  23930  cmssmscld  23931  mbfres2  24224  limciun  24472  dvmptres3  24533  dvmptres2  24539  dvmptntr  24548  dvlipcn  24571  dvlip2  24572  c1liplem1  24573  dvgt0lem1  24579  lhop1lem  24590  dvcnvrelem1  24594  dvcvx  24597  ftc2ditglem  24622  wilthlem2  25627  dchrval  25791  dchrelbas2  25794  egrsubgr  27040  pthdlem1  27528  eupthvdres  27993  eupth2lem3  27994  eupth2  27997  eucrct2eupth  28003  hhssablo  29019  hhssnvt  29021  hhsssh  29025  fnunres1  30337  resf1o  30447  gsummpt2d  30689  symgcom  30729  tocycval  30752  tocycfv  30753  tocycf  30761  tocyc01  30762  cycpm2tr  30763  cycpmconjslem1  30798  cycpmconjslem2  30799  qtophaus  31105  esumcvg  31347  eulerpartlemn  31641  sseqp1  31655  signsvtn0  31842  ftc2re  31871  reprsuc  31888  bnj1385  32106  bnj1326  32300  bnj1321  32301  bnj1442  32323  bnj1450  32324  bnj1463  32329  bnj1529  32344  f1resfz0f1d  32363  pfxwlk  32372  pthhashvtx  32376  cvmliftlem5  32538  cvmliftlem7  32540  cvmliftlem10  32543  cvmliftlem11  32544  cvmliftlem15  32547  cvmlift2lem11  32562  cvmlift2lem12  32563  satffunlem1lem1  32651  satffunlem2lem1  32653  eldm3  32999  funsseq  33013  frecseq123  33121  frr3g  33123  fpr3g  33124  frrlem1  33125  frrlem4  33128  frrlem12  33136  fpr2  33142  frr2  33147  noresle  33202  nosupno  33205  nosupdm  33206  nosupfv  33208  nosupres  33209  nosupbnd1lem1  33210  nosupbnd1lem3  33212  nosupbnd1lem5  33214  nosupbnd1  33216  nosupbnd2  33218  noeta  33224  finixpnum  34906  poimirlem3  34924  poimirlem4  34925  poimirlem9  34930  sdclem2  35044  prdsbnd2  35100  isdivrngo  35255  drngoi  35256  elrefsymrels2  35832  eleqvrels2  35854  dibffval  38303  hdmapffval  38989  hdmapfval  38990  eldiophb  39441  diophrw  39443  diophin  39456  rclexi  40060  rtrclex  40062  rtrclexi  40066  cnvrcl0  40070  dfrtrcl5  40074  dfrcl2  40104  fvmptiunrelexplb0da  40115  sblpnf  40727  fresin2  41513  limsupresuz  42069  limsupvaluz  42074  limsupvaluz2  42104  supcnvlimsup  42106  climrescn  42114  liminfresuz  42150  cncfuni  42254  dvresntr  42287  dvbdfbdioolem1  42298  itgiccshift  42350  itgperiod  42351  dirkercncflem2  42474  fourierdlem46  42522  fourierdlem48  42524  fourierdlem49  42525  fourierdlem58  42534  fourierdlem72  42548  fourierdlem74  42550  fourierdlem75  42551  fourierdlem81  42557  fourierdlem88  42564  fourierdlem89  42565  fourierdlem90  42566  fourierdlem91  42567  fourierdlem92  42568  fourierdlem103  42579  fourierdlem104  42580  fourierdlem112  42588  fouriersw  42601  voncmpl  42988  funcoressn  43362  funressnmo  43366  funressndmafv2rn  43507  f1oresf1orab  43573  isomgreqve  44070  idfusubc0  44216  idfusubc  44217  rngcval  44313  rnghmsubcsetclem1  44326  rngccat  44329  rngcid  44330  rngcidALTV  44342  rngcifuestrc  44348  funcrngcsetc  44349  funcrngcsetcALT  44350  ringcval  44359  rhmsubcsetclem1  44372  ringccat  44375  ringcid  44376  rhmsubcrngclem1  44378  rhmsubcrngc  44380  funcringcsetc  44386  funcringcsetcALTV2lem5  44391  ringcidALTV  44405  funcringcsetclem5ALTV  44414  rhmsubc  44441  rhmsubcALTVlem3  44457  aacllem  44982