Theorem reseq1i 5923

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 5921	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶)

Syntax hints:   = wceq 1541   ↾ cres 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904  df-res 5626

This theorem is referenced by:  reseq12i  5925  resindm  5978  resmpt  5985  resmpt3  5986  resmptf  5987  elimampt  5991  opabresid  5998  rescnvcnv  6151  coires1  6212  fnunres2  6594  fresaunres1  6696  fcoi1  6697  fninfp  7108  fvsnun1  7116  fvsnun2  7117  resoprab  7464  resmpo  7466  elimampo  7483  elrnmpores  7484  ofmres  7916  f1stres  7945  f2ndres  7946  df1st2  8028  df2nd2  8029  fsplitfpar  8048  dftpos2  8173  frrlem12  8227  tfr2a  8314  tfr2b  8315  rdgseg  8341  frsucmpt2  8359  seqomlem2  8370  seqomlem3  8371  seqomlem4  8372  domss2  9049  dffi3  9315  axdc  10412  fpwwe2lem12  10533  seqval  13919  hashgval  14240  hashinf  14242  submefmnd  18803  pgrpsubgsymg  19321  gsumzunsnd  19868  ablfac1b  19984  zzngim  21489  pmatcollpw3lem  22698  txflf  23921  xmsxmet2  24374  msmet2  24375  tmsxpsmopn  24452  isngp2  24512  subgnm  24548  tngngp2  24567  cnfldms  24690  msdcn  24757  oprpiece1res1  24876  oprpiece1res2  24877  isncvsngp  25076  cncms  25282  cnfldcusp  25284  reust  25308  minveclem3a  25354  dvreslem  25837  dvres2lem  25838  dvmptresicc  25844  dvcmulf  25875  mdegfval  25994  psercn  26363  abelth  26378  efcvx  26386  efifo  26483  dfrelog  26501  dvrelog  26573  dvlog  26587  efopnlem2  26593  dvatan  26872  dchrisumlem1  27427  noetasuplem2  27673  noetasuplem3  27674  noetasuplem4  27675  noetainflem2  27677  wlknwwlksnbij  29866  df1stres  32685  df2ndres  32686  padct  32701  ressplusf  32944  ressnm  32945  gsummpt2d  33029  cycpmrn  33112  tocyccntz  33113  cycpmconjslem2  33124  qusima  33373  qqhcn  34004  cnrrext  34023  rrhre  34034  esumcvg  34099  dya2icoseg2  34291  eulerpartgbij  34385  satf0  35416  neibastop2  36405  mptsnunlem  37382  icorempo  37395  poimirlem3  37662  mbfposadd  37706  ftc1anclem3  37734  dvasin  37743  dvacos  37744  prdsbnd2  37834  repwsmet  37873  rrnequiv  37874  inres2  38281  xrnres  38448  xrnres2  38449  xrnres3  38450  diophin  42864  eldioph4b  42903  dnnumch1  43136  aomclem6  43151  radcnvrat  44406  lhe4.4ex1a  44421  dvsid  44423  dvsef  44424  imassmpt  45358  elicores  45632  climresmpt  45756  dvcosre  46009  itgsinexplem1  46051  fourierdlem40  46244  fourierdlem57  46260  fourierdlem58  46261  fourierdlem62  46265  fourierdlem74  46277  fourierdlem75  46278  fourierdlem76  46279  fourierdlem80  46283  fourierdlem84  46287  fourierdlem85  46288  fourierdlem101  46304  fourierdlem102  46305  fourierdlem111  46314  fourierdlem114  46317  fouriersw  46328  fouriercn  46329  volicorescl  46650  fdmdifeqresdif  48441  tposresg  48977  tposrescnv  48978  rescofuf  49193  aacllem  49901