Theorem reseq2i 5102

Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqi.1	|- A = B

Assertion

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

Proof of Theorem reseq2i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 |- A = B
2		reseq2 5100	. 2 |- ( A = B -> ( C |` A ) = ( C |` B ) )
3	1, 2	ax-mp 8	1 |- ( C |` A ) = ( C |` B )

Syntax hints:   = wceq 1649   |` cres 4839

This theorem is referenced by:  reseq12i  5103  rescom  5130  rescnvcnv  5291  resdm2  5319  funcnvres  5481  resasplit  5572  fresaunres2  5574  fresaunres1  5575  resdif  5655  resin  5656  domss2  7225  ordtypelem1  7443  ackbij2lem3  8077  facnn  11523  fac0  11524  ruclem4  12788  setsid  13463  dprd2da  15555  ply1plusgfvi  16591  uptx  17610  txcn  17611  ressxms  18508  ressms  18509  iscmet3lem3  19196  volres  19377  dvlip  19830  dvne0  19848  lhop  19853  dflog2  20411  dfrelog  20416  dvlog  20495  wilthlem2  20805  0pth  21523  2pthlem1  21548  ghsubgolem  21911  zrdivrng  21973  df1stres  24044  df2ndres  24045  hashresfn  24109  sitmcl  24616  divcnvshft  25164  divcnvlin  25165  wfrlem5  25474  frrlem5  25499  isdrngo1  26462  eldioph4b  26762  diophren  26764  seff  27406  sblpnf  27407  bnj1326  29101

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-opab 4227  df-xp 4843  df-res 4849