Theorem reseq1i 5119

Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)

Hypothesis

Ref	Expression
reseqi.1	|- A = B

Assertion

Ref	Expression
reseq1i	|- ( A |` C ) = ( B |` C )

Proof of Theorem reseq1i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 |- A = B
2		reseq1 5117	. 2 |- ( A = B -> ( A |` C ) = ( B |` C ) )
3	1, 2	ax-mp 5	1 |- ( A |` C ) = ( B |` C )

Syntax hints:   = wceq 1454   |` cres 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422  df-res 4864

This theorem is referenced by:  reseq12i  5121  resindm  5167  resmpt  5172  resmpt3  5173  opabresid  5176  rescnvcnv  5316  coires1  5371  fresaunres1  5778  fcoi1  5779  fninfp  6114  fvsnun1  6122  fvsnun2  6123  resoprab  6418  resmpt2  6420  elrnmpt2res  6436  ofmres  6815  f1stres  6841  f2ndres  6842  df1st2  6908  df2nd2  6909  dftpos2  7015  wfrlem14  7074  tfr2a  7138  tfr2b  7139  rdgseg  7165  frsucmpt2  7182  seqomlem2  7193  seqomlem3  7194  seqomlem4  7195  domss2  7756  dffi3  7970  fpwwe2lem13  9092  seqval  12255  hashgval  12549  hashinf  12551  pgrpsubgsymg  17097  gsumzunsnd  17636  ablfac1b  17751  zzngim  19171  pmatcollpw3lem  19855  cnmptid  20724  txflf  21069  xmsxmet2  21522  msmet2  21523  tmsxpsmopn  21600  isngp2  21659  subgnm  21689  tngngp2  21708  cnfldms  21844  msdcn  21907  oprpiece1res1  22027  oprpiece1res2  22028  cncms  22370  cnfldcusp  22372  reust  22388  minveclem3a  22417  minveclem3aOLD  22429  dvreslem  22912  dvres2lem  22913  dvcmulf  22947  mdegfval  23059  psercn  23429  abelth  23444  efcvx  23452  efifo  23544  dfrelog  23563  dvrelog  23630  dvlog  23644  efopnlem2  23650  dvatan  23909  dchrisumlem1  24375  constr3pthlem1  25431  resmptf  28305  df1stres  28332  df2ndres  28333  padct  28355  ressplusf  28459  ressnm  28460  gsummpt2d  28592  qqhcn  28843  cnrrext  28862  rrhre  28873  esumcvg  28955  dya2icoseg2  29148  eulerpartgbij  29253  trpred0  30525  neibastop2  31065  mptsnunlem  31784  icorempt2  31798  poimirlem3  31987  mbfposadd  32032  ftc1anclem3  32063  dvasin  32072  dvacos  32073  prdsbnd2  32171  repwsmet  32210  rrnequiv  32211  diophin  35659  eldioph4b  35698  dnnumch1  35946  aomclem6  35961  radcnvrat  36706  lhe4.4ex1a  36721  dvsid  36723  dvsef  36724  elicores  37672  dvcosre  37818  dvmptresicc  37828  itgsinexplem1  37867  fourierdlem40  38047  fourierdlem57  38064  fourierdlem58  38065  fourierdlem62  38069  fourierdlem74  38081  fourierdlem75  38082  fourierdlem76  38083  fourierdlem80  38087  fourierdlem84  38091  fourierdlem85  38092  fourierdlem101  38108  fourierdlem102  38109  fourierdlem111  38118  fourierdlem114  38121  fouriersw  38132  fouriercn  38133  volicorescl  38412  fdmdifeqresdif  40395  aacllem  40812