Theorem reseq1i 5993

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

Syntax hints:   = wceq 1540   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-res 5697

This theorem is referenced by:  reseq12i  5995  resindm  6048  resmpt  6055  resmpt3  6056  resmptf  6057  elimampt  6061  opabresid  6068  rescnvcnv  6224  coires1  6284  fnunres2  6681  fresaunres1  6781  fcoi1  6782  fninfp  7194  fvsnun1  7202  fvsnun2  7203  resoprab  7551  resmpo  7553  elimampo  7570  elrnmpores  7571  ofmres  8009  f1stres  8038  f2ndres  8039  df1st2  8123  df2nd2  8124  fsplitfpar  8143  dftpos2  8268  frrlem12  8322  wfrlem14OLD  8362  tfr2a  8435  tfr2b  8436  rdgseg  8462  frsucmpt2  8480  seqomlem2  8491  seqomlem3  8492  seqomlem4  8493  domss2  9176  dffi3  9471  axdc  10561  fpwwe2lem12  10682  seqval  14053  hashgval  14372  hashinf  14374  submefmnd  18908  pgrpsubgsymg  19427  gsumzunsnd  19974  ablfac1b  20090  zzngim  21571  pmatcollpw3lem  22789  txflf  24014  xmsxmet2  24469  msmet2  24470  tmsxpsmopn  24550  isngp2  24610  subgnm  24646  tngngp2  24673  cnfldms  24796  msdcn  24863  oprpiece1res1  24982  oprpiece1res2  24983  isncvsngp  25183  cncms  25389  cnfldcusp  25391  reust  25415  minveclem3a  25461  dvreslem  25944  dvres2lem  25945  dvmptresicc  25951  dvcmulf  25982  mdegfval  26101  psercn  26470  abelth  26485  efcvx  26493  efifo  26589  dfrelog  26607  dvrelog  26679  dvlog  26693  efopnlem2  26699  dvatan  26978  dchrisumlem1  27533  noetasuplem2  27779  noetasuplem3  27780  noetasuplem4  27781  noetainflem2  27783  wlknwwlksnbij  29908  df1stres  32713  df2ndres  32714  padct  32731  ressplusf  32948  ressnm  32949  gsummpt2d  33052  cycpmrn  33163  tocyccntz  33164  cycpmconjslem2  33175  qusima  33436  qqhcn  33992  cnrrext  34011  rrhre  34022  esumcvg  34087  dya2icoseg2  34280  eulerpartgbij  34374  satf0  35377  neibastop2  36362  mptsnunlem  37339  icorempo  37352  poimirlem3  37630  mbfposadd  37674  ftc1anclem3  37702  dvasin  37711  dvacos  37712  prdsbnd2  37802  repwsmet  37841  rrnequiv  37842  inres2  38247  xrnres  38403  xrnres2  38404  xrnres3  38405  diophin  42783  eldioph4b  42822  dnnumch1  43056  aomclem6  43071  radcnvrat  44333  lhe4.4ex1a  44348  dvsid  44350  dvsef  44351  imassmpt  45269  elicores  45546  climresmpt  45674  dvcosre  45927  itgsinexplem1  45969  fourierdlem40  46162  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem80  46201  fourierdlem84  46205  fourierdlem85  46206  fourierdlem101  46222  fourierdlem102  46223  fourierdlem111  46232  fourierdlem114  46235  fouriersw  46246  fouriercn  46247  volicorescl  46568  fdmdifeqresdif  48258  tposresg  48778  tposrescnv  48779  rescofuf  48922  aacllem  49320