Theorem reseq2d 5954

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

Syntax hints:   → wi 4   = wceq 1550   ↾ cres 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-in 3902  df-opab 5153  df-xp 5642  df-res 5648

This theorem is referenced by:  reseq12d  5955  imadifssran  6122  resresdm  6205  relresfld  6248  fnunres1  6618  f1orescnv  6807  fococnv2  6818  fvn0ssdmfun  7040  fnressn  7126  fnsnsplit  7153  oprssov  7550  curry1  8067  curry2  8070  dftpos2  8207  frecseq123  8247  fpr3g  8250  frrlem1  8251  frrlem4  8254  frrlem12  8262  fpr2a  8267  wfr3g  8284  dfrecs3  8327  tfrlem16  8348  tfr2ALT  8356  tfr3ALT  8357  on2recsov  8622  sbthlem4  9047  mapunen  9103  hartogslem1  9476  frr3g  9700  frr2  9704  axdc3lem2  10394  fseq1p1m1  13589  resunimafz0  14444  hashf1lem1  14454  relexp0g  15021  relexp0  15022  relexpsucnnr  15024  dfrtrcl2  15061  bpolylem  16050  setsval  17175  idfuval  17881  idfu2nd  17882  resf1st  17899  idfusubc0  17904  idfusubc  17905  setcid  18091  catcisolem  18115  estrcid  18138  funcestrcsetclem5  18148  funcsetcestrclem5  18163  funcsetcestrclem7  18165  1stfval  18195  1stf2  18197  2ndfval  18198  2ndf2  18200  1stfcl  18201  2ndfcl  18202  curf2ndf  18251  hofcl  18263  isps  18572  cnvps  18582  isdir  18602  dirref  18605  tsrdir  18608  frmdval  18857  frmdplusg  18860  gsum2dlem2  19983  dprd2da  20056  dpjval  20070  ablfac1eulem  20086  ablfac1eu  20087  rngcval  20636  rnghmsubcsetclem1  20649  rngccat  20652  rngcid  20653  rngcifuestrc  20657  funcrngcsetc  20658  funcrngcsetcALT  20659  ringcval  20665  rhmsubcsetclem1  20678  ringccat  20681  ringcid  20682  rhmsubcrngclem1  20684  rhmsubcrngc  20686  funcringcsetc  20692  rhmsubc  20707  psrplusg  21958  opsrtoslem2  22078  mdetunilem3  22643  mdetunilem4  22644  mdetunilem9  22649  imacmp  23426  ptuncnv  23836  tgphaus  24146  tsmsres  24173  tsmsxplem1  24182  tsmsxplem2  24183  trust  24258  metreslem  24391  imasdsf1olem  24402  xmspropd  24502  mspropd  24503  imasf1oxms  24518  imasf1oms  24519  nmpropd2  24624  isngp2  24626  ngppropd  24666  tngngp2  24681  cphsscph  25282  cmspropd  25380  cmssmscld  25381  mbfres2  25676  limciun  25925  dvmptres3  25987  dvmptres2  25993  dvmptntr  26002  dvlipcn  26025  dvlip2  26026  c1liplem1  26027  dvgt0lem1  26033  lhop1lem  26044  dvcnvrelem1  26048  dvcvx  26051  ftc2ditglem  26076  wilthlem2  27099  dchrval  27264  dchrelbas2  27267  noresle  27727  nosupcbv  27732  nosupno  27733  nosupdm  27734  nosupfv  27736  nosupres  27737  nosupbnd1lem1  27738  nosupbnd1lem3  27740  nosupbnd1lem5  27742  nosupbnd1  27744  nosupbnd2  27746  noinfcbv  27747  noinfno  27748  noinfdm  27749  noinffv  27751  noinfres  27752  noinfbnd1lem3  27755  noinfbnd1lem5  27757  noinfbnd1  27759  noinfbnd2  27761  noetalem1  27771  norecov  28006  norec2ov  28016  egrsubgr  29413  dfpth2  29864  pthdlem1  29901  eupthvdres  30372  eupth2lem3  30373  eupth2  30376  eucrct2eupth  30382  hhssablo  31401  hhssnvt  31403  hhsssh  31407  fresunsn  32766  fressupp  32829  resf1o  32871  gsummpt2d  33179  gsumpart  33193  symgcom  33213  tocycval  33238  tocycfv  33239  tocycf  33247  tocyc01  33248  cycpm2tr  33249  cycpmconjslem1  33284  cycpmconjslem2  33285  nsgqusf1o  33548  extvval  33772  extvfval  33773  extvfvcl  33777  qtophaus  34077  esumcvg  34327  eulerpartlemn  34622  sseqp1  34636  signsvtn0  34811  ftc2re  34839  reprsuc  34856  bnj1385  35074  bnj1326  35268  bnj1321  35269  bnj1442  35291  bnj1450  35292  bnj1463  35297  bnj1529  35312  f1resfz0f1d  35402  pfxwlk  35412  pthhashvtx  35416  cvmliftlem5  35577  cvmliftlem7  35579  cvmliftlem10  35582  cvmliftlem11  35583  cvmliftlem15  35586  cvmlift2lem11  35601  cvmlift2lem12  35602  satffunlem1lem1  35690  satffunlem2lem1  35692  eldm3  36049  funsseq  36056  finixpnum  38042  poimirlem3  38060  poimirlem4  38061  poimirlem9  38066  sdclem2  38179  prdsbnd2  38232  isdivrngo  38387  drngoi  38388  elrefsymrels2  39090  eleqvrels2  39113  dibffval  41702  hdmapffval  42388  hdmapfval  42389  eqresfnbd  42789  dvun  42906  eldiophb  43276  diophrw  43278  diophin  43291  tfsconcatrev  43863  ofoafg  43869  resisoeq45d  43934  rclexi  44129  rtrclex  44131  rtrclexi  44135  cnvrcl0  44139  dfrtrcl5  44143  dfrcl2  44188  fvmptiunrelexplb0da  44199  sblpnf  44824  fresin2  45688  limsupresuz  46215  limsupvaluz  46220  limsupvaluz2  46250  supcnvlimsup  46252  climrescn  46260  liminfresuz  46296  cncfuni  46398  dvresntr  46430  dvbdfbdioolem1  46440  itgiccshift  46492  itgperiod  46493  dirkercncflem2  46616  fourierdlem46  46664  fourierdlem48  46666  fourierdlem49  46667  fourierdlem58  46676  fourierdlem72  46690  fourierdlem74  46692  fourierdlem75  46693  fourierdlem81  46699  fourierdlem88  46706  fourierdlem89  46707  fourierdlem90  46708  fourierdlem91  46709  fourierdlem92  46710  fourierdlem103  46721  fourierdlem104  46722  fourierdlem112  46730  fouriersw  46743  voncmpl  47133  funcoressn  47574  funressnmo  47578  f1cof1blem  47606  funfocofob  47610  funressndmafv2rn  47755  f1oresf1orab  47821  upgrimpths  48469  isubgrgrim  48489  stgrfv  48513  gpgov  48602  rngcidALTV  48834  rhmsubcALTVlem3  48843  funcringcsetcALTV2lem5  48854  ringcidALTV  48868  funcringcsetclem5ALTV  48877  itcoval  49221  itcoval0mpt  49226  itcovalendof  49229  idfu1sta  49660  idfu2nda  49662  imaidfu2  49670  idfullsubc  49720  dfswapf2  49820  oppc1stf  49847  oppc2ndf  49848  1stfpropd  49849  2ndfpropd  49850  fucofvalg  49877  fucof1  49881  fucofvalne  49884  opf2fval  49964  idfudiag1  50084  aacllem  50360