Theorem reseq1d 5395

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

Syntax hints:   → wi 4   = wceq 1483   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-res 5126

This theorem is referenced by:  reseq12d  5397  fun2ssres  5931  funcnvres2  5969  fresin  6073  fresaunres2  6076  offres  7163  itunifval  9238  hsmex  9254  gruima  9624  fseq1p1m1  12414  ltweuz  12760  rlimres  14289  lo1res  14290  lo1resb  14295  rlimresb  14296  o1resb  14297  bitsf1ocnv  15166  fsets  15891  setsres  15901  setscom  15903  sscres  16483  resfval2  16553  estrres  16779  psgnunilem5  17914  gsumzres  18310  gsumzsplit  18327  gsum2dlem2  18370  dpjidcl  18457  pgpfaclem1  18480  pwssplit2  19060  pwssplit3  19061  znle2  19902  phssip  20003  mamures  20196  ofco2  20257  mdetunilem9  20426  mdetmul  20429  smadiadetglem1  20477  smadiadetglem2  20478  tmdgsum  21899  tsmsval2  21933  tsmsres  21947  tsmssplit  21955  imasdsf1olem  22178  tmslem  22287  sranlm  22488  srabn  23156  mbflimsup  23433  dvres  23675  dvres3a  23678  dvnres  23694  cpnres  23700  dvcmul  23707  dvcmulf  23708  dvcobr  23709  dvmptres3  23719  dvmptres2  23725  dvcnvlem  23739  dvlip2  23758  ftc2ditglem  23808  aannenlem1  24083  eff1olem  24294  resqrtcn  24490  sqrtcn  24491  rlimcnp2  24693  jensenlem2  24714  ex-res  27298  rabfodom  29344  resf1o  29505  submatres  29872  zhmnrg  30011  indf1ofs  30088  carsggect  30380  fibp1  30463  actfunsnf1o  30682  cvmliftlem10  31276  cvmlift2lem6  31290  cvmlift2lem12  31296  trpredeq1  31720  trpredeq2  31721  trpredeq3  31722  poimirlem3  33412  ftc1anclem8  33492  ftc2nc  33494  cocnv  33520  cnpwstotbnd  33596  drngoi  33750  eldioph2  37325  itgpowd  37800  dvsconst  38529  disjf1o  39378  cncfmptss  39819  limsupresuz  39935  liminfresuz  40016  dvmptresicc  40134  itgsinexplem1  40169  itgcoscmulx  40185  itgiccshift  40196  itgperiod  40197  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem28  40352  fourierdlem42  40366  fourierdlem78  40401  fourierdlem81  40404  fourierdlem83  40406  fourierdlem84  40407  fourierdlem90  40413  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  sge0resrnlem  40620  ismeannd  40684  0ome  40743  hoidmvlelem3  40811  hoidmvlelem4  40812  funcrngcsetc  41998  funcringcsetc  42035  rhmsubclem1  42086  rhmsubcALTVlem1  42104  aacllem  42547