Theorem reseq1d 5999

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

Syntax hints:   → wi 4   = wceq 1537   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-in 3970  df-res 5701

This theorem is referenced by:  reseq12d  6001  fun2ssres  6613  funcnvres2  6648  fresin  6778  fresaunres2  6781  offres  8007  itunifval  10454  hsmex  10470  gruima  10840  fseq1p1m1  13635  ltweuz  13999  rlimres  15591  lo1res  15592  lo1resb  15597  rlimresb  15598  o1resb  15599  bitsf1ocnv  16478  fsets  17203  setsres  17212  setscom  17214  sscres  17871  resfval2  17944  estrres  18195  symgvalstruct  19429  symgvalstructOLD  19430  gsumzres  19942  gsumzsplit  19960  gsum2dlem2  20004  dpjidcl  20093  pgpfaclem1  20116  funcrngcsetc  20657  funcringcsetc  20691  rhmsubclem1  20702  pwssplit2  21077  pwssplit3  21078  znle2  21590  phssip  21694  mamures  22417  ofco2  22473  mdetunilem9  22642  mdetmul  22645  smadiadetglem1  22693  smadiadetglem2  22694  tmdgsum  24119  tsmsval2  24154  tsmsres  24168  tsmssplit  24176  imasdsf1olem  24399  tmslem  24510  tmslemOLD  24511  sranlm  24721  cmssmscld  25398  srabn  25408  cmscsscms  25421  mbflimsup  25715  dvres  25961  dvres3a  25964  dvmptresicc  25966  dvnres  25982  cpnres  25988  dvcmul  25996  dvcmulf  25997  dvcobr  25998  dvcobrOLD  25999  dvmptres3  26009  dvmptres2  26015  dvcnvlem  26029  dvlip2  26049  ftc2ditglem  26101  itgpowd  26106  aannenlem1  26385  eff1olem  26605  resqrtcn  26807  sqrtcn  26808  rlimcnp2  27024  jensenlem2  27046  ex-res  30470  rabfodom  32533  resf1o  32748  tocycfvres1  33113  tocycfvres2  33114  cycpmconjvlem  33144  cycpmconjslem2  33158  cyc3conja  33160  ply1gsumz  33599  lbsdiflsp0  33654  submatres  33767  zhmnrg  33928  indf1ofs  34007  carsggect  34300  fibp1  34383  actfunsnf1o  34598  cvmliftlem10  35279  cvmlift2lem6  35293  cvmlift2lem12  35299  satf  35338  poimirlem3  37610  ftc1anclem8  37687  ftc2nc  37689  cocnv  37712  cnpwstotbnd  37784  drngoi  37938  aks6d1c6lem2  42153  aks6d1c6lem4  42155  eldioph2  42750  dvsconst  44326  disjf1o  45134  cncfmptss  45543  limsupresuz  45659  liminfresuz  45740  itgsinexplem1  45910  itgcoscmulx  45925  itgiccshift  45936  itgperiod  45937  dirkeritg  46058  dirkercncflem2  46060  dirkercncflem4  46062  fourierdlem16  46079  fourierdlem21  46084  fourierdlem22  46085  fourierdlem28  46091  fourierdlem42  46105  fourierdlem78  46140  fourierdlem81  46143  fourierdlem83  46145  fourierdlem84  46146  fourierdlem90  46152  fourierdlem93  46155  fourierdlem103  46165  fourierdlem104  46166  sge0resrnlem  46359  ismeannd  46423  0ome  46485  hoidmvlelem3  46553  hoidmvlelem4  46554  rhmsubcALTVlem1  48125  aacllem  49032