Theorem reseq1d 5968

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091  df-res 5662

This theorem is used by:  reseq12d  5970  fun2ssres  6585  funcnvres2  6620  fresin  6751  fresaunres2  6754  offres  7995  itunifval  10497  hsmex  10513  gruima  10890  fseq1p1m1  13735  ltweuz  14107  rlimres  15730  lo1res  15731  lo1resb  15736  rlimresb  15737  o1resb  15738  bitsf1ocnv  16619  fsets  17352  setsres  17361  setscom  17363  sscres  18003  resfval2  18073  estrres  18318  symgvalstruct  19616  gsumzres  20128  gsumzsplit  20146  gsum2dlem2  20190  dpjidcl  20279  pgpfaclem1  20302  funcrngcsetc  20897  funcringcsetc  20931  rhmsubclem1  20942  pwssplit2  21340  pwssplit3  21341  znle2  21864  phssip  21969  mamures  22717  ofco2  22771  mdetunilem9  22940  mdetmul  22943  smadiadetglem1  22991  smadiadetglem2  22992  tmdgsum  24419  tsmsval2  24454  tsmsres  24468  tsmssplit  24476  imasdsf1olem  24697  tmslem  24806  sranlm  25008  cmssmscld  25676  srabn  25686  cmscsscms  25699  mbflimsup  25992  dvres  26236  dvres3a  26239  dvmptresicc  26241  dvnres  26256  cpnres  26262  dvcmul  26269  dvcmulf  26270  dvcobr  26271  dvmptres3  26281  dvmptres2  26287  dvcnvlem  26301  dvlip2  26320  ftc2ditglem  26370  itgpowd  26375  aannenlem1  26660  eff1olem  26881  resqrtcn  27082  sqrtcn  27083  rlimcnp2  27299  jensenlem2  27320  ex-res  31047  rabfodom  33148  padct  33357  resf1o  33368  indf1ofs  33479  tocycfvres1  33717  tocycfvres2  33718  cycpmconjvlem  33748  cycpmconjslem2  33762  cyc3conja  33764  gsumind  33952  ply1gsumz  34177  evlextv  34220  lbsdiflsp0  34304  submatres  34484  zhmnrg  34643  carsggect  34996  fibp1  35079  actfunsnf1o  35279  cvmliftlem10  36145  cvmlift2lem6  36159  cvmlift2lem12  36165  satf  36204  poimirlem3  38634  ftc1anclem8  38711  ftc2nc  38713  cocnv  38752  cnpwstotbnd  38824  drngoi  38978  aks6d1c6lem2  43314  aks6d1c6lem4  43316  eldioph2  43866  dvsconst  45407  disjf1o  46299  cncfmptss  46692  limsupresuz  46806  liminfresuz  46887  itgsinexplem1  47057  itgcoscmulx  47072  itgiccshift  47083  itgperiod  47084  dirkeritg  47205  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem16  47226  fourierdlem21  47231  fourierdlem22  47232  fourierdlem28  47238  fourierdlem42  47252  fourierdlem78  47287  fourierdlem81  47290  fourierdlem83  47292  fourierdlem84  47293  fourierdlem90  47299  fourierdlem93  47302  fourierdlem103  47312  fourierdlem104  47313  sge0resrnlem  47506  ismeannd  47570  0ome  47632  hoidmvlelem3  47700  hoidmvlelem4  47701  rhmsubcALTVlem1  49471  aacllem  51107