Theorem reseq1i 5965

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

This proof depends on syntax axioms:   = 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:  reseq12i  5967  resindmOLD  6019  resmpt  6028  resmpt3  6029  resmptf  6030  elimampt  6034  opabresid  6041  rescnvcnv  6205  coires1  6266  fnunres2  6652  fresaunres1  6755  fcoi1  6756  fninfp  7179  fvsnun1  7187  fvsnun2  7188  resoprab  7538  resmpo  7540  elimampo  7557  elrnmpores  7558  ofmres  7996  f1stres  8025  f2ndres  8026  df1st2  8111  df2nd2  8112  fsplitfpar  8131  dftpos2  8263  frrlem12  8318  tfr2a  8406  tfr2b  8407  rdgseg  8433  frsucmpt2  8451  seqomlem2  8464  seqomlem3  8465  seqomlem4  8466  domss2  9158  dffi3  9426  axdc  10602  fpwwe2lem12  10730  seqval  14158  hashgval  14480  hashinf  14482  submefmnd  19096  pgrpsubgsymg  19628  gsumzunsnd  20175  ablfac1b  20291  zzngim  21863  pmatcollpw3lem  23106  txflf  24330  xmsxmet2  24783  msmet2  24784  tmsxpsmopn  24861  isngp2  24921  subgnm  24957  tngngp2  24976  cnfldms  25099  msdcn  25166  oprpiece1res1  25277  oprpiece1res2  25278  isncvsngp  25475  cncms  25681  cnfldcusp  25683  reust  25707  minveclem3a  25753  dvreslem  26234  dvres2lem  26235  dvmptresicc  26241  dvcmulf  26270  mdegfval  26385  psercn  26758  abelth  26773  efcvx  26781  efifo  26880  dfrelog  26898  dvrelog  26970  dvlog  26984  efopnlem2  26990  dvatan  27268  dchrisumlem1  27821  noetasuplem2  28096  noetasuplem3  28097  noetasuplem4  28098  noetainflem2  28100  wlknwwlksnbij  30482  df1stres  33344  df2ndres  33345  padct  33357  ressplusf  33570  ressnm  33571  gsummpt2d  33656  cycpmrn  33750  tocyccntz  33751  cycpmconjslem2  33762  qusima  34005  qqhcn  34669  cnrrext  34688  rrhre  34699  esumcvg  34764  dya2icoseg2  34956  eulerpartgbij  35050  srepdflem1  36004  satf0  36223  neibastop2  37241  mptsnunlem  38354  icorempo  38367  poimirlem3  38634  mbfposadd  38678  ftc1anclem3  38706  dvasin  38715  dvacos  38716  prdsbnd2  38822  repwsmet  38861  rrnequiv  38862  inres2  39272  xrnres  39450  xrnres2  39451  xrnres3  39452  diophin  43876  eldioph4b  43911  dnnumch1  44144  aomclem6  44154  radcnvrat  45391  lhe4.4ex1a  45406  dvsid  45408  dvsef  45409  imassmpt  46367  elicores  46638  climresmpt  46762  dvcosre  47015  itgsinexplem1  47057  fourierdlem40  47250  fourierdlem57  47266  fourierdlem58  47267  fourierdlem62  47271  fourierdlem74  47283  fourierdlem75  47284  fourierdlem76  47285  fourierdlem80  47289  fourierdlem84  47293  fourierdlem85  47294  fourierdlem101  47310  fourierdlem102  47311  fourierdlem111  47320  fourierdlem114  47323  fouriersw  47334  fouriercn  47335  volicorescl  47656  fdmdifeqresdif  49547  tposresg  50084  tposrescnv  50085  rescofuf  50301  aacllem  51107