Theorem reseq2d 5818

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

Syntax hints:   → wi 4   = wceq 1538   ↾ cres 5521

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888  df-opab 5093  df-xp 5525  df-res 5531

This theorem is referenced by:  reseq12d  5819  resresdm  6057  relresfld  6095  f1orescnv  6605  fococnv2  6615  fvn0ssdmfun  6819  fnressn  6897  fnsnsplit  6923  oprssov  7297  curry1  7782  curry2  7785  dftpos2  7892  wrecseq123  7931  wfr3g  7936  wfrlem1  7937  wfrlem4  7941  wfrlem14  7951  wfr2a  7955  dfrecs3  7992  tfrlem16  8012  tfr2ALT  8020  tfr3ALT  8021  sbthlem4  8614  mapunen  8670  hartogslem1  8990  axdc3lem2  9862  fseq1p1m1  12976  resunimafz0  13799  hashf1lem1  13809  relexp0g  14373  relexp0  14374  relexpsucnnr  14376  dfrtrcl2  14413  bpolylem  15394  setsval  16505  idfuval  17138  idfu2nd  17139  resf1st  17156  setcid  17338  catcisolem  17358  estrcid  17376  funcestrcsetclem5  17386  funcsetcestrclem5  17401  funcsetcestrclem7  17403  1stfval  17433  1stf2  17435  2ndfval  17436  2ndf2  17438  1stfcl  17439  2ndfcl  17440  curf2ndf  17489  hofcl  17501  isps  17804  cnvps  17814  isdir  17834  dirref  17837  tsrdir  17840  frmdval  18008  frmdplusg  18011  gsum2dlem2  19084  dprd2da  19157  dpjval  19171  ablfac1eulem  19187  ablfac1eu  19188  psrplusg  20619  opsrtoslem2  20724  mdetunilem3  21219  mdetunilem4  21220  mdetunilem9  21225  imacmp  22002  ptuncnv  22412  tgphaus  22722  tsmsres  22749  tsmsxplem1  22758  tsmsxplem2  22759  trust  22835  metreslem  22969  imasdsf1olem  22980  xmspropd  23080  mspropd  23081  imasf1oxms  23096  imasf1oms  23097  nmpropd2  23201  isngp2  23203  ngppropd  23243  tngngp2  23258  cphsscph  23855  cmspropd  23953  cmssmscld  23954  mbfres2  24249  limciun  24497  dvmptres3  24559  dvmptres2  24565  dvmptntr  24574  dvlipcn  24597  dvlip2  24598  c1liplem1  24599  dvgt0lem1  24605  lhop1lem  24616  dvcnvrelem1  24620  dvcvx  24623  ftc2ditglem  24648  wilthlem2  25654  dchrval  25818  dchrelbas2  25821  egrsubgr  27067  pthdlem1  27555  eupthvdres  28020  eupth2lem3  28021  eupth2  28024  eucrct2eupth  28030  hhssablo  29046  hhssnvt  29048  hhsssh  29052  fnunres1  30369  fressupp  30448  resf1o  30492  gsummpt2d  30734  gsumpart  30740  symgcom  30777  tocycval  30800  tocycfv  30801  tocycf  30809  tocyc01  30810  cycpm2tr  30811  cycpmconjslem1  30846  cycpmconjslem2  30847  qtophaus  31189  esumcvg  31455  eulerpartlemn  31749  sseqp1  31763  signsvtn0  31950  ftc2re  31979  reprsuc  31996  bnj1385  32214  bnj1326  32408  bnj1321  32409  bnj1442  32431  bnj1450  32432  bnj1463  32437  bnj1529  32452  f1resfz0f1d  32471  pfxwlk  32483  pthhashvtx  32487  cvmliftlem5  32649  cvmliftlem7  32651  cvmliftlem10  32654  cvmliftlem11  32655  cvmliftlem15  32658  cvmlift2lem11  32673  cvmlift2lem12  32674  satffunlem1lem1  32762  satffunlem2lem1  32764  eldm3  33110  funsseq  33124  frecseq123  33232  frr3g  33234  fpr3g  33235  frrlem1  33236  frrlem4  33239  frrlem12  33247  fpr2  33253  frr2  33258  noresle  33313  nosupno  33316  nosupdm  33317  nosupfv  33319  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1lem3  33323  nosupbnd1lem5  33325  nosupbnd1  33327  nosupbnd2  33329  noeta  33335  finixpnum  35042  poimirlem3  35060  poimirlem4  35061  poimirlem9  35066  sdclem2  35180  prdsbnd2  35233  isdivrngo  35388  drngoi  35389  elrefsymrels2  35965  eleqvrels2  35987  dibffval  38436  hdmapffval  39122  hdmapfval  39123  eldiophb  39698  diophrw  39700  diophin  39713  rclexi  40315  rtrclex  40317  rtrclexi  40321  cnvrcl0  40325  dfrtrcl5  40329  dfrcl2  40375  fvmptiunrelexplb0da  40386  sblpnf  41014  fresin2  41796  limsupresuz  42345  limsupvaluz  42350  limsupvaluz2  42380  supcnvlimsup  42382  climrescn  42390  liminfresuz  42426  cncfuni  42528  dvresntr  42560  dvbdfbdioolem1  42570  itgiccshift  42622  itgperiod  42623  dirkercncflem2  42746  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem58  42806  fourierdlem72  42820  fourierdlem74  42822  fourierdlem75  42823  fourierdlem81  42829  fourierdlem88  42836  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem92  42840  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fouriersw  42873  voncmpl  43260  funcoressn  43634  funressnmo  43638  funressndmafv2rn  43779  f1oresf1orab  43845  isomgreqve  44343  idfusubc0  44489  idfusubc  44490  rngcval  44586  rnghmsubcsetclem1  44599  rngccat  44602  rngcid  44603  rngcidALTV  44615  rngcifuestrc  44621  funcrngcsetc  44622  funcrngcsetcALT  44623  ringcval  44632  rhmsubcsetclem1  44645  ringccat  44648  ringcid  44649  rhmsubcrngclem1  44651  rhmsubcrngc  44653  funcringcsetc  44659  funcringcsetcALTV2lem5  44664  ringcidALTV  44678  funcringcsetclem5ALTV  44687  rhmsubc  44714  rhmsubcALTVlem3  44730  itcoval  45075  itcoval0mpt  45080  itcovalendof  45083  aacllem  45329