Theorem reseq1d 5979

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

Syntax hints:   → wi 4   = wceq 1570   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913  df-res 5675

This theorem is referenced by:  reseq12d  5981  fun2ssres  6583  funcnvres2  6618  fresin  6749  fresaunres2  6752  offres  7981  itunifval  10401  hsmex  10417  gruima  10788  fseq1p1m1  13628  ltweuz  13999  rlimres  15611  lo1res  15612  lo1resb  15617  rlimresb  15618  o1resb  15619  bitsf1ocnv  16503  fsets  17230  setsres  17239  setscom  17241  sscres  17881  resfval2  17951  estrres  18196  symgvalstruct  19468  gsumzres  19980  gsumzsplit  19998  gsum2dlem2  20042  dpjidcl  20131  pgpfaclem1  20154  funcrngcsetc  20726  funcringcsetc  20760  rhmsubclem1  20771  pwssplit2  21162  pwssplit3  21163  znle2  21684  phssip  21789  mamures  22535  ofco2  22589  mdetunilem9  22758  mdetmul  22761  smadiadetglem1  22809  smadiadetglem2  22810  tmdgsum  24233  tsmsval2  24268  tsmsres  24282  tsmssplit  24290  imasdsf1olem  24511  tmslem  24620  sranlm  24822  cmssmscld  25490  srabn  25500  cmscsscms  25513  mbflimsup  25806  dvres  26051  dvres3a  26054  dvmptresicc  26056  dvnres  26071  cpnres  26077  dvcmul  26084  dvcmulf  26085  dvcobr  26086  dvmptres3  26096  dvmptres2  26102  dvcnvlem  26116  dvlip2  26135  ftc2ditglem  26185  itgpowd  26190  aannenlem1  26470  eff1olem  26691  resqrtcn  26892  sqrtcn  26893  rlimcnp2  27109  jensenlem2  27130  ex-res  30770  rabfodom  32829  padct  33041  resf1o  33053  indf1ofs  33164  tocycfvres1  33408  tocycfvres2  33409  cycpmconjvlem  33439  cycpmconjslem2  33453  cyc3conja  33455  gsumind  33643  ply1gsumz  33867  evlextv  33910  lbsdiflsp0  33994  submatres  34174  zhmnrg  34333  carsggect  34686  fibp1  34769  actfunsnf1o  34969  cvmliftlem10  35764  cvmlift2lem6  35778  cvmlift2lem12  35784  satf  35823  poimirlem3  38252  ftc1anclem8  38329  ftc2nc  38331  cocnv  38354  cnpwstotbnd  38426  drngoi  38580  aks6d1c6lem2  42916  aks6d1c6lem4  42918  eldioph2  43473  dvsconst  45020  disjf1o  45889  cncfmptss  46283  limsupresuz  46397  liminfresuz  46478  itgsinexplem1  46648  itgcoscmulx  46663  itgiccshift  46674  itgperiod  46675  dirkeritg  46796  dirkercncflem2  46798  dirkercncflem4  46800  fourierdlem16  46817  fourierdlem21  46822  fourierdlem22  46823  fourierdlem28  46829  fourierdlem42  46843  fourierdlem78  46878  fourierdlem81  46881  fourierdlem83  46883  fourierdlem84  46884  fourierdlem90  46890  fourierdlem93  46893  fourierdlem103  46903  fourierdlem104  46904  sge0resrnlem  47097  ismeannd  47161  0ome  47223  hoidmvlelem3  47291  hoidmvlelem4  47292  rhmsubcALTVlem1  49023  aacllem  50578