Theorem reseq1i 5890

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

Syntax hints:   = wceq 1539   ↾ cres 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895  df-res 5602

This theorem is referenced by:  reseq12i  5892  resindm  5943  resmpt  5948  resmpt3  5949  resmptf  5950  opabresid  5960  opabresidOLD  5962  rescnvcnv  6112  coires1  6172  fresaunres1  6656  fcoi1  6657  fninfp  7055  fvsnun1  7063  fvsnun2  7064  resoprab  7401  resmpo  7403  elrnmpores  7420  ofmres  7836  f1stres  7864  f2ndres  7865  df1st2  7947  df2nd2  7948  fsplitfpar  7968  dftpos2  8068  frrlem12  8122  wfrlem14OLD  8162  tfr2a  8235  tfr2b  8236  rdgseg  8262  frsucmpt2  8280  seqomlem2  8291  seqomlem3  8292  seqomlem4  8293  domss2  8932  dffi3  9199  fpwwe2lem12  10407  seqval  13741  hashgval  14056  hashinf  14058  submefmnd  18543  pgrpsubgsymg  19026  gsumzunsnd  19566  ablfac1b  19682  zzngim  20769  pmatcollpw3lem  21941  txflf  23166  xmsxmet2  23621  msmet2  23622  tmsxpsmopn  23702  isngp2  23762  subgnm  23798  tngngp2  23825  cnfldms  23948  msdcn  24013  oprpiece1res1  24123  oprpiece1res2  24124  isncvsngp  24322  cncms  24528  cnfldcusp  24530  reust  24554  minveclem3a  24600  dvreslem  25082  dvres2lem  25083  dvmptresicc  25089  dvcmulf  25118  mdegfval  25236  psercn  25594  abelth  25609  efcvx  25617  efifo  25712  dfrelog  25730  dvrelog  25801  dvlog  25815  efopnlem2  25821  dvatan  26094  dchrisumlem1  26646  wlknwwlksnbij  28262  elimampt  30982  fnunres2  31024  df1stres  31045  df2ndres  31046  padct  31063  ressplusf  31244  ressnm  31245  gsummpt2d  31318  cycpmrn  31419  tocyccntz  31420  cycpmconjslem2  31431  qusima  31603  qqhcn  31950  cnrrext  31969  rrhre  31980  esumcvg  32063  dya2icoseg2  32254  eulerpartgbij  32348  satf0  33343  noetasuplem2  33946  noetasuplem3  33947  noetasuplem4  33948  noetainflem2  33950  neibastop2  34559  mptsnunlem  35518  icorempo  35531  poimirlem3  35789  mbfposadd  35833  ftc1anclem3  35861  dvasin  35870  dvacos  35871  prdsbnd2  35962  repwsmet  36001  rrnequiv  36002  inres2  36393  xrnres  36535  xrnres2  36536  xrnres3  36537  diophin  40601  eldioph4b  40640  dnnumch1  40876  aomclem6  40891  radcnvrat  41939  lhe4.4ex1a  41954  dvsid  41956  dvsef  41957  imassmpt  42817  elicores  43078  climresmpt  43207  dvcosre  43460  itgsinexplem1  43502  fourierdlem40  43695  fourierdlem57  43711  fourierdlem58  43712  fourierdlem62  43716  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem84  43738  fourierdlem85  43739  fourierdlem101  43755  fourierdlem102  43756  fourierdlem111  43765  fourierdlem114  43768  fouriersw  43779  fouriercn  43780  volicorescl  44098  fdmdifeqresdif  45688  aacllem  46516