Theorem reseq2d 5932

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

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

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905  df-opab 5156  df-xp 5625  df-res 5631

This theorem is referenced by:  reseq12d  5933  imadifssran  6103  resresdm  6185  relresfld  6228  fnunres1  6598  f1orescnv  6783  fococnv2  6794  fvn0ssdmfun  7013  fnressn  7097  fnsnsplit  7124  oprssov  7521  curry1  8040  curry2  8043  dftpos2  8179  frecseq123  8218  fpr3g  8221  frrlem1  8222  frrlem4  8225  frrlem12  8233  fpr2a  8238  wfr3g  8255  dfrecs3  8298  tfrlem16  8318  tfr2ALT  8326  tfr3ALT  8327  on2recsov  8589  sbthlem4  9010  mapunen  9066  hartogslem1  9435  frr3g  9656  frr2  9660  axdc3lem2  10349  fseq1p1m1  13500  resunimafz0  14354  hashf1lem1  14364  relexp0g  14931  relexp0  14932  relexpsucnnr  14934  dfrtrcl2  14971  bpolylem  15957  setsval  17080  idfuval  17785  idfu2nd  17786  resf1st  17803  idfusubc0  17808  idfusubc  17809  setcid  17995  catcisolem  18019  estrcid  18042  funcestrcsetclem5  18052  funcsetcestrclem5  18067  funcsetcestrclem7  18069  1stfval  18099  1stf2  18101  2ndfval  18102  2ndf2  18104  1stfcl  18105  2ndfcl  18106  curf2ndf  18155  hofcl  18167  isps  18476  cnvps  18486  isdir  18506  dirref  18509  tsrdir  18512  frmdval  18761  frmdplusg  18764  gsum2dlem2  19885  dprd2da  19958  dpjval  19972  ablfac1eulem  19988  ablfac1eu  19989  rngcval  20535  rnghmsubcsetclem1  20548  rngccat  20551  rngcid  20552  rngcifuestrc  20556  funcrngcsetc  20557  funcrngcsetcALT  20558  ringcval  20564  rhmsubcsetclem1  20577  ringccat  20580  ringcid  20581  rhmsubcrngclem1  20583  rhmsubcrngc  20585  funcringcsetc  20591  rhmsubc  20606  psrplusg  21875  opsrtoslem2  21992  mdetunilem3  22530  mdetunilem4  22531  mdetunilem9  22536  imacmp  23313  ptuncnv  23723  tgphaus  24033  tsmsres  24060  tsmsxplem1  24069  tsmsxplem2  24070  trust  24145  metreslem  24278  imasdsf1olem  24289  xmspropd  24389  mspropd  24390  imasf1oxms  24405  imasf1oms  24406  nmpropd2  24511  isngp2  24513  ngppropd  24553  tngngp2  24568  cphsscph  25179  cmspropd  25277  cmssmscld  25278  mbfres2  25574  limciun  25823  dvmptres3  25888  dvmptres2  25894  dvmptntr  25903  dvlipcn  25927  dvlip2  25928  c1liplem1  25929  dvgt0lem1  25935  lhop1lem  25946  dvcnvrelem1  25950  dvcvx  25953  ftc2ditglem  25980  wilthlem2  27007  dchrval  27173  dchrelbas2  27176  noresle  27637  nosupcbv  27642  nosupno  27643  nosupdm  27644  nosupfv  27646  nosupres  27647  nosupbnd1lem1  27648  nosupbnd1lem3  27650  nosupbnd1lem5  27652  nosupbnd1  27654  nosupbnd2  27656  noinfcbv  27657  noinfno  27658  noinfdm  27659  noinffv  27661  noinfres  27662  noinfbnd1lem3  27665  noinfbnd1lem5  27667  noinfbnd1  27669  noinfbnd2  27671  noetalem1  27681  norecov  27891  norec2ov  27901  egrsubgr  29257  dfpth2  29709  pthdlem1  29746  eupthvdres  30217  eupth2lem3  30218  eupth2  30221  eucrct2eupth  30227  hhssablo  31245  hhssnvt  31247  hhsssh  31251  fressupp  32673  resf1o  32717  gsummpt2d  33036  gsumpart  33044  symgcom  33059  tocycval  33084  tocycfv  33085  tocycf  33093  tocyc01  33094  cycpm2tr  33095  cycpmconjslem1  33130  cycpmconjslem2  33131  nsgqusf1o  33388  extvval  33582  extvfval  33583  extvfvcl  33587  qtophaus  33870  esumcvg  34120  eulerpartlemn  34415  sseqp1  34429  signsvtn0  34604  ftc2re  34632  reprsuc  34649  bnj1385  34865  bnj1326  35059  bnj1321  35060  bnj1442  35082  bnj1450  35083  bnj1463  35088  bnj1529  35103  f1resfz0f1d  35179  pfxwlk  35189  pthhashvtx  35193  cvmliftlem5  35354  cvmliftlem7  35356  cvmliftlem10  35359  cvmliftlem11  35360  cvmliftlem15  35363  cvmlift2lem11  35378  cvmlift2lem12  35379  satffunlem1lem1  35467  satffunlem2lem1  35469  eldm3  35826  funsseq  35833  finixpnum  37665  poimirlem3  37683  poimirlem4  37684  poimirlem9  37689  sdclem2  37802  prdsbnd2  37855  isdivrngo  38010  drngoi  38011  elrefsymrels2  38685  eleqvrels2  38708  dibffval  41259  hdmapffval  41945  hdmapfval  41946  eqresfnbd  42350  dvun  42477  eldiophb  42874  diophrw  42876  diophin  42889  tfsconcatrev  43465  ofoafg  43471  resisoeq45d  43537  rclexi  43732  rtrclex  43734  rtrclexi  43738  cnvrcl0  43742  dfrtrcl5  43746  dfrcl2  43791  fvmptiunrelexplb0da  43802  sblpnf  44427  fresin2  45293  limsupresuz  45825  limsupvaluz  45830  limsupvaluz2  45860  supcnvlimsup  45862  climrescn  45870  liminfresuz  45906  cncfuni  46008  dvresntr  46040  dvbdfbdioolem1  46050  itgiccshift  46102  itgperiod  46103  dirkercncflem2  46226  fourierdlem46  46274  fourierdlem48  46276  fourierdlem49  46277  fourierdlem58  46286  fourierdlem72  46300  fourierdlem74  46302  fourierdlem75  46303  fourierdlem81  46309  fourierdlem88  46316  fourierdlem89  46317  fourierdlem90  46318  fourierdlem91  46319  fourierdlem92  46320  fourierdlem103  46331  fourierdlem104  46332  fourierdlem112  46340  fouriersw  46353  voncmpl  46743  funcoressn  47166  funressnmo  47170  f1cof1blem  47198  funfocofob  47202  funressndmafv2rn  47347  f1oresf1orab  47413  upgrimpths  48033  isubgrgrim  48053  stgrfv  48077  gpgov  48166  rngcidALTV  48398  rhmsubcALTVlem3  48407  funcringcsetcALTV2lem5  48418  ringcidALTV  48432  funcringcsetclem5ALTV  48441  itcoval  48786  itcoval0mpt  48791  itcovalendof  48794  idfu1sta  49226  idfu2nda  49228  imaidfu2  49236  idfullsubc  49286  dfswapf2  49386  oppc1stf  49413  oppc2ndf  49414  1stfpropd  49415  2ndfpropd  49416  fucofvalg  49443  fucof1  49447  fucofvalne  49450  opf2fval  49530  idfudiag1  49650  aacllem  49926