Theorem reseq2d 5963

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

Syntax hints:   → wi 4   = wceq 1559   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3911  df-opab 5162  df-xp 5651  df-res 5657

This theorem is referenced by:  reseq12d  5964  imadifssran  6133  resresdm  6216  relresfld  6259  fnunres1  6629  f1orescnv  6818  fococnv2  6829  fvn0ssdmfun  7051  fnressn  7137  fnsnsplit  7164  oprssov  7561  curry1  8078  curry2  8081  dftpos2  8218  frecseq123  8258  fpr3g  8261  frrlem1  8262  frrlem4  8265  frrlem12  8273  fpr2a  8278  wfr3g  8295  dfrecs3  8338  tfrlem16  8359  tfr2ALT  8367  tfr3ALT  8368  on2recsov  8633  sbthlem4  9058  mapunen  9114  hartogslem1  9487  frr3g  9711  frr2  9715  axdc3lem2  10405  fseq1p1m1  13600  resunimafz0  14455  hashf1lem1  14465  relexp0g  15032  relexp0  15033  relexpsucnnr  15035  dfrtrcl2  15072  bpolylem  16061  setsval  17186  idfuval  17892  idfu2nd  17893  resf1st  17910  idfusubc0  17915  idfusubc  17916  setcid  18102  catcisolem  18126  estrcid  18149  funcestrcsetclem5  18159  funcsetcestrclem5  18174  funcsetcestrclem7  18176  1stfval  18206  1stf2  18208  2ndfval  18209  2ndf2  18211  1stfcl  18212  2ndfcl  18213  curf2ndf  18262  hofcl  18274  isps  18583  cnvps  18593  isdir  18613  dirref  18616  tsrdir  18619  frmdval  18868  frmdplusg  18871  gsum2dlem2  19994  dprd2da  20067  dpjval  20081  ablfac1eulem  20097  ablfac1eu  20098  rngcval  20647  rnghmsubcsetclem1  20660  rngccat  20663  rngcid  20664  rngcifuestrc  20668  funcrngcsetc  20669  funcrngcsetcALT  20670  ringcval  20676  rhmsubcsetclem1  20689  ringccat  20692  ringcid  20693  rhmsubcrngclem1  20695  rhmsubcrngc  20697  funcringcsetc  20703  rhmsubc  20718  psrplusg  21969  opsrtoslem2  22089  mdetunilem3  22654  mdetunilem4  22655  mdetunilem9  22660  imacmp  23437  ptuncnv  23847  tgphaus  24157  tsmsres  24184  tsmsxplem1  24193  tsmsxplem2  24194  trust  24269  metreslem  24402  imasdsf1olem  24413  xmspropd  24513  mspropd  24514  imasf1oxms  24529  imasf1oms  24530  nmpropd2  24635  isngp2  24637  ngppropd  24677  tngngp2  24692  cphsscph  25293  cmspropd  25391  cmssmscld  25392  mbfres2  25687  limciun  25936  dvmptres3  25998  dvmptres2  26004  dvmptntr  26013  dvlipcn  26036  dvlip2  26037  c1liplem1  26038  dvgt0lem1  26044  lhop1lem  26055  dvcnvrelem1  26059  dvcvx  26062  ftc2ditglem  26087  wilthlem2  27110  dchrval  27275  dchrelbas2  27278  noresle  27738  nosupcbv  27743  nosupno  27744  nosupdm  27745  nosupfv  27747  nosupres  27748  nosupbnd1lem1  27749  nosupbnd1lem3  27751  nosupbnd1lem5  27753  nosupbnd1  27755  nosupbnd2  27757  noinfcbv  27758  noinfno  27759  noinfdm  27760  noinffv  27762  noinfres  27763  noinfbnd1lem3  27766  noinfbnd1lem5  27768  noinfbnd1  27770  noinfbnd2  27772  noetalem1  27782  norecov  28017  norec2ov  28027  egrsubgr  29424  dfpth2  29875  pthdlem1  29912  eupthvdres  30383  eupth2lem3  30384  eupth2  30387  eucrct2eupth  30393  hhssablo  31412  hhssnvt  31414  hhsssh  31418  fresunsn  32777  fressupp  32840  resf1o  32882  gsummpt2d  33190  gsumpart  33204  symgcom  33224  tocycval  33249  tocycfv  33250  tocycf  33258  tocyc01  33259  cycpm2tr  33260  cycpmconjslem1  33295  cycpmconjslem2  33296  nsgqusf1o  33563  extvval  33789  extvfval  33790  extvfvcl  33794  qtophaus  34094  esumcvg  34344  eulerpartlemn  34639  sseqp1  34653  signsvtn0  34828  ftc2re  34856  reprsuc  34873  bnj1385  35091  bnj1326  35285  bnj1321  35286  bnj1442  35308  bnj1450  35309  bnj1463  35314  bnj1529  35329  f1resfz0f1d  35428  pfxwlk  35438  pthhashvtx  35442  cvmliftlem5  35603  cvmliftlem7  35605  cvmliftlem10  35608  cvmliftlem11  35609  cvmliftlem15  35612  cvmlift2lem11  35627  cvmlift2lem12  35628  satffunlem1lem1  35716  satffunlem2lem1  35718  eldm3  36075  funsseq  36082  finixpnum  38068  poimirlem3  38086  poimirlem4  38087  poimirlem9  38092  sdclem2  38205  prdsbnd2  38258  isdivrngo  38413  drngoi  38414  elrefsymrels2  39116  eleqvrels2  39139  dibffval  41728  hdmapffval  42414  hdmapfval  42415  eqresfnbd  42815  dvun  42932  eldiophb  43302  diophrw  43304  diophin  43317  tfsconcatrev  43889  ofoafg  43895  resisoeq45d  43960  rclexi  44155  rtrclex  44157  rtrclexi  44161  cnvrcl0  44165  dfrtrcl5  44169  dfrcl2  44214  fvmptiunrelexplb0da  44225  sblpnf  44850  fresin2  45714  limsupresuz  46241  limsupvaluz  46246  limsupvaluz2  46276  supcnvlimsup  46278  climrescn  46286  liminfresuz  46322  cncfuni  46424  dvresntr  46456  dvbdfbdioolem1  46466  itgiccshift  46518  itgperiod  46519  dirkercncflem2  46642  fourierdlem46  46690  fourierdlem48  46692  fourierdlem49  46693  fourierdlem58  46702  fourierdlem72  46716  fourierdlem74  46718  fourierdlem75  46719  fourierdlem81  46725  fourierdlem88  46732  fourierdlem89  46733  fourierdlem90  46734  fourierdlem91  46735  fourierdlem92  46736  fourierdlem103  46747  fourierdlem104  46748  fourierdlem112  46756  fouriersw  46769  voncmpl  47159  funcoressn  47600  funressnmo  47604  f1cof1blem  47632  funfocofob  47636  funressndmafv2rn  47781  f1oresf1orab  47847  upgrimpths  48495  isubgrgrim  48515  stgrfv  48539  gpgov  48628  rngcidALTV  48860  rhmsubcALTVlem3  48869  funcringcsetcALTV2lem5  48880  ringcidALTV  48894  funcringcsetclem5ALTV  48903  itcoval  49247  itcoval0mpt  49252  itcovalendof  49255  idfu1sta  49686  idfu2nda  49688  imaidfu2  49696  idfullsubc  49746  dfswapf2  49846  oppc1stf  49873  oppc2ndf  49874  1stfpropd  49875  2ndfpropd  49876  fucofvalg  49903  fucof1  49907  fucofvalne  49910  opf2fval  49990  idfudiag1  50110  aacllem  50386