Theorem reseq1i 5940

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

Syntax hints:   = wceq 1542   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896  df-res 5643

This theorem is referenced by:  reseq12i  5942  resindm  5995  resmpt  6002  resmpt3  6003  resmptf  6004  elimampt  6008  opabresid  6015  rescnvcnv  6168  coires1  6229  fnunres2  6611  fresaunres1  6713  fcoi1  6714  fninfp  7129  fvsnun1  7137  fvsnun2  7138  resoprab  7485  resmpo  7487  elimampo  7504  elrnmpores  7505  ofmres  7937  f1stres  7966  f2ndres  7967  df1st2  8048  df2nd2  8049  fsplitfpar  8068  dftpos2  8193  frrlem12  8247  tfr2a  8334  tfr2b  8335  rdgseg  8361  frsucmpt2  8379  seqomlem2  8390  seqomlem3  8391  seqomlem4  8392  domss2  9074  dffi3  9344  axdc  10443  fpwwe2lem12  10565  seqval  13974  hashgval  14295  hashinf  14297  submefmnd  18863  pgrpsubgsymg  19384  gsumzunsnd  19931  ablfac1b  20047  zzngim  21532  pmatcollpw3lem  22748  txflf  23971  xmsxmet2  24424  msmet2  24425  tmsxpsmopn  24502  isngp2  24562  subgnm  24598  tngngp2  24617  cnfldms  24740  msdcn  24807  oprpiece1res1  24918  oprpiece1res2  24919  isncvsngp  25116  cncms  25322  cnfldcusp  25324  reust  25348  minveclem3a  25394  dvreslem  25876  dvres2lem  25877  dvmptresicc  25883  dvcmulf  25912  mdegfval  26027  psercn  26391  abelth  26406  efcvx  26414  efifo  26511  dfrelog  26529  dvrelog  26601  dvlog  26615  efopnlem2  26621  dvatan  26899  dchrisumlem1  27452  noetasuplem2  27698  noetasuplem3  27699  noetasuplem4  27700  noetainflem2  27702  wlknwwlksnbij  29956  df1stres  32777  df2ndres  32778  padct  32791  ressplusf  33023  ressnm  33024  gsummpt2d  33110  cycpmrn  33204  tocyccntz  33205  cycpmconjslem2  33216  qusima  33468  qqhcn  34135  cnrrext  34154  rrhre  34165  esumcvg  34230  dya2icoseg2  34422  eulerpartgbij  34516  satf0  35554  neibastop2  36543  mptsnunlem  37654  icorempo  37667  poimirlem3  37944  mbfposadd  37988  ftc1anclem3  38016  dvasin  38025  dvacos  38026  prdsbnd2  38116  repwsmet  38155  rrnequiv  38156  inres2  38568  xrnres  38746  xrnres2  38747  xrnres3  38748  diophin  43204  eldioph4b  43239  dnnumch1  43472  aomclem6  43487  radcnvrat  44741  lhe4.4ex1a  44756  dvsid  44758  dvsef  44759  imassmpt  45691  elicores  45963  climresmpt  46087  dvcosre  46340  itgsinexplem1  46382  fourierdlem40  46575  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem80  46614  fourierdlem84  46618  fourierdlem85  46619  fourierdlem101  46635  fourierdlem102  46636  fourierdlem111  46645  fourierdlem114  46648  fouriersw  46659  fouriercn  46660  volicorescl  46981  fdmdifeqresdif  48818  tposresg  49353  tposrescnv  49354  rescofuf  49568  aacllem  50276