Theorem reseq1d 5969

Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq1d	⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

Proof of Theorem reseq1d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq1 5964	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906  df-res 5663

This theorem is used by:  reseq12d  5971  fun2ssres  6577  funcnvres2  6612  fresin  6743  fresaunres2  6746  offres  7984  itunifval  10475  hsmex  10491  gruima  10868  fseq1p1m1  13712  ltweuz  14084  rlimres  15705  lo1res  15706  lo1resb  15711  rlimresb  15712  o1resb  15713  bitsf1ocnv  16594  fsets  17327  setsres  17336  setscom  17338  sscres  17978  resfval2  18048  estrres  18293  symgvalstruct  19591  gsumzres  20103  gsumzsplit  20121  gsum2dlem2  20165  dpjidcl  20254  pgpfaclem1  20277  funcrngcsetc  20872  funcringcsetc  20906  rhmsubclem1  20917  pwssplit2  21315  pwssplit3  21316  znle2  21839  phssip  21944  mamures  22692  ofco2  22746  mdetunilem9  22915  mdetmul  22918  smadiadetglem1  22966  smadiadetglem2  22967  tmdgsum  24394  tsmsval2  24429  tsmsres  24443  tsmssplit  24451  imasdsf1olem  24672  tmslem  24781  sranlm  24983  cmssmscld  25651  srabn  25661  cmscsscms  25674  mbflimsup  25967  dvres  26211  dvres3a  26214  dvmptresicc  26216  dvnres  26231  cpnres  26237  dvcmul  26244  dvcmulf  26245  dvcobr  26246  dvmptres3  26256  dvmptres2  26262  dvcnvlem  26276  dvlip2  26295  ftc2ditglem  26345  itgpowd  26350  aannenlem1  26637  eff1olem  26858  resqrtcn  27059  sqrtcn  27060  rlimcnp2  27276  jensenlem2  27297  ex-res  31024  rabfodom  33083  padct  33292  resf1o  33304  indf1ofs  33415  tocycfvres1  33653  tocycfvres2  33654  cycpmconjvlem  33684  cycpmconjslem2  33698  cyc3conja  33700  gsumind  33888  ply1gsumz  34113  evlextv  34156  lbsdiflsp0  34240  submatres  34420  zhmnrg  34579  carsggect  34933  fibp1  35016  actfunsnf1o  35216  cvmliftlem10  36028  cvmlift2lem6  36042  cvmlift2lem12  36048  satf  36087  poimirlem3  38509  ftc1anclem8  38586  ftc2nc  38588  cocnv  38627  cnpwstotbnd  38699  drngoi  38853  aks6d1c6lem2  43189  aks6d1c6lem4  43191  eldioph2  43726  dvsconst  45273  disjf1o  46149  cncfmptss  46543  limsupresuz  46657  liminfresuz  46738  itgsinexplem1  46908  itgcoscmulx  46923  itgiccshift  46934  itgperiod  46935  dirkeritg  47056  dirkercncflem2  47058  dirkercncflem4  47060  fourierdlem16  47077  fourierdlem21  47082  fourierdlem22  47083  fourierdlem28  47089  fourierdlem42  47103  fourierdlem78  47138  fourierdlem81  47141  fourierdlem83  47143  fourierdlem84  47144  fourierdlem90  47150  fourierdlem93  47153  fourierdlem103  47163  fourierdlem104  47164  sge0resrnlem  47357  ismeannd  47421  0ome  47483  hoidmvlelem3  47551  hoidmvlelem4  47552  rhmsubcALTVlem1  49322  aacllem  50883