Theorem reseq1i 5995

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

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
reseq1i	⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 ⊢ 𝐴 = 𝐵
2		reseq1 5993	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1536   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969  df-res 5700

This theorem is referenced by:  reseq12i  5997  resindm  6049  resmpt  6056  resmpt3  6057  resmptf  6058  elimampt  6062  opabresid  6069  rescnvcnv  6225  coires1  6285  fnunres2  6681  fresaunres1  6781  fcoi1  6782  fninfp  7193  fvsnun1  7201  fvsnun2  7202  resoprab  7550  resmpo  7552  elimampo  7569  elrnmpores  7570  ofmres  8007  f1stres  8036  f2ndres  8037  df1st2  8121  df2nd2  8122  fsplitfpar  8141  dftpos2  8266  frrlem12  8320  wfrlem14OLD  8360  tfr2a  8433  tfr2b  8434  rdgseg  8460  frsucmpt2  8478  seqomlem2  8489  seqomlem3  8490  seqomlem4  8491  domss2  9174  dffi3  9468  fpwwe2lem12  10679  seqval  14049  hashgval  14368  hashinf  14370  submefmnd  18920  pgrpsubgsymg  19441  gsumzunsnd  19988  ablfac1b  20104  zzngim  21588  pmatcollpw3lem  22804  txflf  24029  xmsxmet2  24484  msmet2  24485  tmsxpsmopn  24565  isngp2  24625  subgnm  24661  tngngp2  24688  cnfldms  24811  msdcn  24876  oprpiece1res1  24995  oprpiece1res2  24996  isncvsngp  25196  cncms  25402  cnfldcusp  25404  reust  25428  minveclem3a  25474  dvreslem  25958  dvres2lem  25959  dvmptresicc  25965  dvcmulf  25996  mdegfval  26115  psercn  26484  abelth  26499  efcvx  26507  efifo  26603  dfrelog  26621  dvrelog  26693  dvlog  26707  efopnlem2  26713  dvatan  26992  dchrisumlem1  27547  noetasuplem2  27793  noetasuplem3  27794  noetasuplem4  27795  noetainflem2  27797  wlknwwlksnbij  29917  df1stres  32718  df2ndres  32719  padct  32736  ressplusf  32932  ressnm  32933  gsummpt2d  33034  cycpmrn  33145  tocyccntz  33146  cycpmconjslem2  33157  qusima  33415  qqhcn  33953  cnrrext  33972  rrhre  33983  esumcvg  34066  dya2icoseg2  34259  eulerpartgbij  34353  satf0  35356  neibastop2  36343  mptsnunlem  37320  icorempo  37333  poimirlem3  37609  mbfposadd  37653  ftc1anclem3  37681  dvasin  37690  dvacos  37691  prdsbnd2  37781  repwsmet  37820  rrnequiv  37821  inres2  38226  xrnres  38383  xrnres2  38384  xrnres3  38385  readvrec  42370  diophin  42759  eldioph4b  42798  dnnumch1  43032  aomclem6  43047  radcnvrat  44309  lhe4.4ex1a  44324  dvsid  44326  dvsef  44327  imassmpt  45207  elicores  45485  climresmpt  45614  dvcosre  45867  itgsinexplem1  45909  fourierdlem40  46102  fourierdlem57  46118  fourierdlem58  46119  fourierdlem62  46123  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem80  46141  fourierdlem84  46145  fourierdlem85  46146  fourierdlem101  46162  fourierdlem102  46163  fourierdlem111  46172  fourierdlem114  46175  fouriersw  46186  fouriercn  46187  volicorescl  46508  fdmdifeqresdif  48186  aacllem  49031