Theorem reseq2d 5888

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

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3898  df-opab 5141  df-xp 5594  df-res 5600

This theorem is referenced by:  reseq12d  5889  resresdm  6133  relresfld  6176  f1orescnv  6727  fococnv2  6737  fvn0ssdmfun  6946  fnressn  7024  fnsnsplit  7050  oprssov  7432  curry1  7928  curry2  7931  dftpos2  8043  frecseq123  8082  fpr3g  8085  frrlem1  8086  frrlem4  8089  frrlem12  8097  fpr2a  8102  wrecseq123OLD  8115  wfr3g  8122  wfrlem1OLD  8123  wfrlem4OLD  8127  wfrlem14OLD  8137  wfr2aOLD  8141  dfrecs3  8187  dfrecs3OLD  8188  tfrlem16  8208  tfr2ALT  8216  tfr3ALT  8217  sbthlem4  8842  mapunen  8898  hartogslem1  9262  frr3g  9498  frr2  9502  axdc3lem2  10191  fseq1p1m1  13312  resunimafz0  14138  hashf1lem1  14149  hashf1lem1OLD  14150  relexp0g  14714  relexp0  14715  relexpsucnnr  14717  dfrtrcl2  14754  bpolylem  15739  setsval  16849  idfuval  17572  idfu2nd  17573  resf1st  17590  setcid  17782  catcisolem  17806  estrcid  17831  funcestrcsetclem5  17842  funcsetcestrclem5  17857  funcsetcestrclem7  17859  1stfval  17889  1stf2  17891  2ndfval  17892  2ndf2  17894  1stfcl  17895  2ndfcl  17896  curf2ndf  17946  hofcl  17958  isps  18267  cnvps  18277  isdir  18297  dirref  18300  tsrdir  18303  frmdval  18471  frmdplusg  18474  gsum2dlem2  19553  dprd2da  19626  dpjval  19640  ablfac1eulem  19656  ablfac1eu  19657  psrplusg  21131  opsrtoslem2  21244  mdetunilem3  21744  mdetunilem4  21745  mdetunilem9  21750  imacmp  22529  ptuncnv  22939  tgphaus  23249  tsmsres  23276  tsmsxplem1  23285  tsmsxplem2  23286  trust  23362  metreslem  23496  imasdsf1olem  23507  xmspropd  23607  mspropd  23608  imasf1oxms  23626  imasf1oms  23627  nmpropd2  23732  isngp2  23734  ngppropd  23774  tngngp2  23797  cphsscph  24396  cmspropd  24494  cmssmscld  24495  mbfres2  24790  limciun  25039  dvmptres3  25101  dvmptres2  25107  dvmptntr  25116  dvlipcn  25139  dvlip2  25140  c1liplem1  25141  dvgt0lem1  25147  lhop1lem  25158  dvcnvrelem1  25162  dvcvx  25165  ftc2ditglem  25190  wilthlem2  26199  dchrval  26363  dchrelbas2  26366  egrsubgr  27625  pthdlem1  28113  eupthvdres  28578  eupth2lem3  28579  eupth2  28582  eucrct2eupth  28588  hhssablo  29604  hhssnvt  29606  hhsssh  29610  fnunres1  30924  fressupp  31001  resf1o  31044  gsummpt2d  31288  gsumpart  31294  symgcom  31331  tocycval  31354  tocycfv  31355  tocycf  31363  tocyc01  31364  cycpm2tr  31365  cycpmconjslem1  31400  cycpmconjslem2  31401  nsgqusf1o  31580  qtophaus  31765  esumcvg  32033  eulerpartlemn  32327  sseqp1  32341  signsvtn0  32528  ftc2re  32557  reprsuc  32574  bnj1385  32791  bnj1326  32985  bnj1321  32986  bnj1442  33008  bnj1450  33009  bnj1463  33014  bnj1529  33029  f1resfz0f1d  33051  pfxwlk  33064  pthhashvtx  33068  cvmliftlem5  33230  cvmliftlem7  33232  cvmliftlem10  33235  cvmliftlem11  33236  cvmliftlem15  33239  cvmlift2lem11  33254  cvmlift2lem12  33255  satffunlem1lem1  33343  satffunlem2lem1  33345  eldm3  33707  funsseq  33721  on2recsov  33806  noresle  33879  nosupcbv  33884  nosupno  33885  nosupdm  33886  nosupfv  33888  nosupres  33889  nosupbnd1lem1  33890  nosupbnd1lem3  33892  nosupbnd1lem5  33894  nosupbnd1  33896  nosupbnd2  33898  noinfcbv  33899  noinfno  33900  noinfdm  33901  noinffv  33903  noinfres  33904  noinfbnd1lem3  33907  noinfbnd1lem5  33909  noinfbnd1  33911  noinfbnd2  33913  noetalem1  33923  norecov  34083  norec2ov  34093  finixpnum  35741  poimirlem3  35759  poimirlem4  35760  poimirlem9  35765  sdclem2  35879  prdsbnd2  35932  isdivrngo  36087  drngoi  36088  elrefsymrels2  36662  eleqvrels2  36684  dibffval  39133  hdmapffval  39819  hdmapfval  39820  eldiophb  40559  diophrw  40561  diophin  40574  rclexi  41176  rtrclex  41178  rtrclexi  41182  cnvrcl0  41186  dfrtrcl5  41190  dfrcl2  41235  fvmptiunrelexplb0da  41246  sblpnf  41881  fresin2  42661  limsupresuz  43198  limsupvaluz  43203  limsupvaluz2  43233  supcnvlimsup  43235  climrescn  43243  liminfresuz  43279  cncfuni  43381  dvresntr  43413  dvbdfbdioolem1  43423  itgiccshift  43475  itgperiod  43476  dirkercncflem2  43599  fourierdlem46  43647  fourierdlem48  43649  fourierdlem49  43650  fourierdlem58  43659  fourierdlem72  43673  fourierdlem74  43675  fourierdlem75  43676  fourierdlem81  43682  fourierdlem88  43689  fourierdlem89  43690  fourierdlem90  43691  fourierdlem91  43692  fourierdlem92  43693  fourierdlem103  43704  fourierdlem104  43705  fourierdlem112  43713  fouriersw  43726  voncmpl  44113  funcoressn  44487  funressnmo  44491  f1cof1blem  44519  funfocofob  44521  funressndmafv2rn  44666  f1oresf1orab  44732  isomgreqve  45229  idfusubc0  45375  idfusubc  45376  rngcval  45472  rnghmsubcsetclem1  45485  rngccat  45488  rngcid  45489  rngcidALTV  45501  rngcifuestrc  45507  funcrngcsetc  45508  funcrngcsetcALT  45509  ringcval  45518  rhmsubcsetclem1  45531  ringccat  45534  ringcid  45535  rhmsubcrngclem1  45537  rhmsubcrngc  45539  funcringcsetc  45545  funcringcsetcALTV2lem5  45550  ringcidALTV  45564  funcringcsetclem5ALTV  45573  rhmsubc  45600  rhmsubcALTVlem3  45616  itcoval  45959  itcoval0mpt  45964  itcovalendof  45967  aacllem  46457