Theorem reseq2d 5944

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

Syntax hints:   → wi 4   = wceq 1542   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896  df-opab 5148  df-xp 5637  df-res 5643

This theorem is referenced by:  reseq12d  5945  imadifssran  6115  resresdm  6197  relresfld  6240  fnunres1  6610  f1orescnv  6795  fococnv2  6806  fvn0ssdmfun  7026  fnressn  7112  fnsnsplit  7139  oprssov  7536  curry1  8054  curry2  8057  dftpos2  8193  frecseq123  8232  fpr3g  8235  frrlem1  8236  frrlem4  8239  frrlem12  8247  fpr2a  8252  wfr3g  8269  dfrecs3  8312  tfrlem16  8332  tfr2ALT  8340  tfr3ALT  8341  on2recsov  8604  sbthlem4  9028  mapunen  9084  hartogslem1  9457  frr3g  9680  frr2  9684  axdc3lem2  10373  fseq1p1m1  13552  resunimafz0  14407  hashf1lem1  14417  relexp0g  14984  relexp0  14985  relexpsucnnr  14987  dfrtrcl2  15024  bpolylem  16013  setsval  17137  idfuval  17843  idfu2nd  17844  resf1st  17861  idfusubc0  17866  idfusubc  17867  setcid  18053  catcisolem  18077  estrcid  18100  funcestrcsetclem5  18110  funcsetcestrclem5  18125  funcsetcestrclem7  18127  1stfval  18157  1stf2  18159  2ndfval  18160  2ndf2  18162  1stfcl  18163  2ndfcl  18164  curf2ndf  18213  hofcl  18225  isps  18534  cnvps  18544  isdir  18564  dirref  18567  tsrdir  18570  frmdval  18819  frmdplusg  18822  gsum2dlem2  19946  dprd2da  20019  dpjval  20033  ablfac1eulem  20049  ablfac1eu  20050  rngcval  20595  rnghmsubcsetclem1  20608  rngccat  20611  rngcid  20612  rngcifuestrc  20616  funcrngcsetc  20617  funcrngcsetcALT  20618  ringcval  20624  rhmsubcsetclem1  20637  ringccat  20640  ringcid  20641  rhmsubcrngclem1  20643  rhmsubcrngc  20645  funcringcsetc  20651  rhmsubc  20666  psrplusg  21916  opsrtoslem2  22034  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  imacmp  23362  ptuncnv  23772  tgphaus  24082  tsmsres  24109  tsmsxplem1  24118  tsmsxplem2  24119  trust  24194  metreslem  24327  imasdsf1olem  24338  xmspropd  24438  mspropd  24439  imasf1oxms  24454  imasf1oms  24455  nmpropd2  24560  isngp2  24562  ngppropd  24602  tngngp2  24617  cphsscph  25218  cmspropd  25316  cmssmscld  25317  mbfres2  25612  limciun  25861  dvmptres3  25923  dvmptres2  25929  dvmptntr  25938  dvlipcn  25961  dvlip2  25962  c1liplem1  25963  dvgt0lem1  25969  lhop1lem  25980  dvcnvrelem1  25984  dvcvx  25987  ftc2ditglem  26012  wilthlem2  27032  dchrval  27197  dchrelbas2  27200  noresle  27661  nosupcbv  27666  nosupno  27667  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd1  27678  nosupbnd2  27680  noinfcbv  27681  noinfno  27682  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd1  27693  noinfbnd2  27695  noetalem1  27705  norecov  27939  norec2ov  27949  egrsubgr  29346  dfpth2  29797  pthdlem1  29834  eupthvdres  30305  eupth2lem3  30306  eupth2  30309  eucrct2eupth  30315  hhssablo  31334  hhssnvt  31336  hhsssh  31340  fresunsn  32698  fressupp  32761  resf1o  32803  gsummpt2d  33110  gsumpart  33124  symgcom  33144  tocycval  33169  tocycfv  33170  tocycf  33178  tocyc01  33179  cycpm2tr  33180  cycpmconjslem1  33215  cycpmconjslem2  33216  nsgqusf1o  33476  extvval  33675  extvfval  33676  extvfvcl  33680  qtophaus  33980  esumcvg  34230  eulerpartlemn  34525  sseqp1  34539  signsvtn0  34714  ftc2re  34742  reprsuc  34759  bnj1385  34974  bnj1326  35168  bnj1321  35169  bnj1442  35191  bnj1450  35192  bnj1463  35197  bnj1529  35212  f1resfz0f1d  35296  pfxwlk  35306  pthhashvtx  35310  cvmliftlem5  35471  cvmliftlem7  35473  cvmliftlem10  35476  cvmliftlem11  35477  cvmliftlem15  35480  cvmlift2lem11  35495  cvmlift2lem12  35496  satffunlem1lem1  35584  satffunlem2lem1  35586  eldm3  35943  funsseq  35950  finixpnum  37926  poimirlem3  37944  poimirlem4  37945  poimirlem9  37950  sdclem2  38063  prdsbnd2  38116  isdivrngo  38271  drngoi  38272  elrefsymrels2  38974  eleqvrels2  38997  dibffval  41586  hdmapffval  42272  hdmapfval  42273  eqresfnbd  42673  dvun  42791  eldiophb  43189  diophrw  43191  diophin  43204  tfsconcatrev  43776  ofoafg  43782  resisoeq45d  43847  rclexi  44042  rtrclex  44044  rtrclexi  44048  cnvrcl0  44052  dfrtrcl5  44056  dfrcl2  44101  fvmptiunrelexplb0da  44112  sblpnf  44737  fresin2  45602  limsupresuz  46131  limsupvaluz  46136  limsupvaluz2  46166  supcnvlimsup  46168  climrescn  46176  liminfresuz  46212  cncfuni  46314  dvresntr  46346  dvbdfbdioolem1  46356  itgiccshift  46408  itgperiod  46409  dirkercncflem2  46532  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem58  46592  fourierdlem72  46606  fourierdlem74  46608  fourierdlem75  46609  fourierdlem81  46615  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fouriersw  46659  voncmpl  47049  funcoressn  47490  funressnmo  47494  f1cof1blem  47522  funfocofob  47526  funressndmafv2rn  47671  f1oresf1orab  47737  upgrimpths  48385  isubgrgrim  48405  stgrfv  48429  gpgov  48518  rngcidALTV  48750  rhmsubcALTVlem3  48759  funcringcsetcALTV2lem5  48770  ringcidALTV  48784  funcringcsetclem5ALTV  48793  itcoval  49137  itcoval0mpt  49142  itcovalendof  49145  idfu1sta  49576  idfu2nda  49578  imaidfu2  49586  idfullsubc  49636  dfswapf2  49736  oppc1stf  49763  oppc2ndf  49764  1stfpropd  49765  2ndfpropd  49766  fucofvalg  49793  fucof1  49797  fucofvalne  49800  opf2fval  49880  idfudiag1  50000  aacllem  50276