Theorem reseq1i 5946

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

Syntax hints:   = wceq 1540   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921  df-res 5650

This theorem is referenced by:  reseq12i  5948  resindm  6001  resmpt  6008  resmpt3  6009  resmptf  6010  elimampt  6014  opabresid  6021  rescnvcnv  6177  coires1  6237  fnunres2  6631  fresaunres1  6733  fcoi1  6734  fninfp  7148  fvsnun1  7156  fvsnun2  7157  resoprab  7507  resmpo  7509  elimampo  7526  elrnmpores  7527  ofmres  7963  f1stres  7992  f2ndres  7993  df1st2  8077  df2nd2  8078  fsplitfpar  8097  dftpos2  8222  frrlem12  8276  tfr2a  8363  tfr2b  8364  rdgseg  8390  frsucmpt2  8408  seqomlem2  8419  seqomlem3  8420  seqomlem4  8421  domss2  9100  dffi3  9382  axdc  10474  fpwwe2lem12  10595  seqval  13977  hashgval  14298  hashinf  14300  submefmnd  18822  pgrpsubgsymg  19339  gsumzunsnd  19886  ablfac1b  20002  zzngim  21462  pmatcollpw3lem  22670  txflf  23893  xmsxmet2  24347  msmet2  24348  tmsxpsmopn  24425  isngp2  24485  subgnm  24521  tngngp2  24540  cnfldms  24663  msdcn  24730  oprpiece1res1  24849  oprpiece1res2  24850  isncvsngp  25049  cncms  25255  cnfldcusp  25257  reust  25281  minveclem3a  25327  dvreslem  25810  dvres2lem  25811  dvmptresicc  25817  dvcmulf  25848  mdegfval  25967  psercn  26336  abelth  26351  efcvx  26359  efifo  26456  dfrelog  26474  dvrelog  26546  dvlog  26560  efopnlem2  26566  dvatan  26845  dchrisumlem1  27400  noetasuplem2  27646  noetasuplem3  27647  noetasuplem4  27648  noetainflem2  27650  wlknwwlksnbij  29818  df1stres  32627  df2ndres  32628  padct  32643  ressplusf  32885  ressnm  32886  gsummpt2d  32989  cycpmrn  33100  tocyccntz  33101  cycpmconjslem2  33112  qusima  33379  qqhcn  33981  cnrrext  34000  rrhre  34011  esumcvg  34076  dya2icoseg2  34269  eulerpartgbij  34363  satf0  35359  neibastop2  36349  mptsnunlem  37326  icorempo  37339  poimirlem3  37617  mbfposadd  37661  ftc1anclem3  37689  dvasin  37698  dvacos  37699  prdsbnd2  37789  repwsmet  37828  rrnequiv  37829  inres2  38234  xrnres  38388  xrnres2  38389  xrnres3  38390  diophin  42760  eldioph4b  42799  dnnumch1  43033  aomclem6  43048  radcnvrat  44303  lhe4.4ex1a  44318  dvsid  44320  dvsef  44321  imassmpt  45256  elicores  45531  climresmpt  45657  dvcosre  45910  itgsinexplem1  45952  fourierdlem40  46145  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem80  46184  fourierdlem84  46188  fourierdlem85  46189  fourierdlem101  46205  fourierdlem102  46206  fourierdlem111  46215  fourierdlem114  46218  fouriersw  46229  fouriercn  46230  volicorescl  46551  fdmdifeqresdif  48330  tposresg  48866  tposrescnv  48867  rescofuf  49082  aacllem  49790