Theorem reseq2i 5103

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 5101	. 2 |- ( A = B -> ( C |` A ) = ( C |` B ) )
3	1, 2	ax-mp 5	1 |- ( C |` A ) = ( C |` B )

Syntax hints:   = wceq 1364   |` cres 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-opab 4348  df-xp 4842  df-res 4848

This theorem is referenced by:  reseq12i  5104  rescom  5132  rescnvcnv  5298  resdm2  5325  funcnvres  5484  resasplit  5578  fresaunres2  5580  fresaunres1  5581  resdif  5658  resin  5659  residpr  5883  domss2  7466  ordtypelem1  7728  ackbij2lem3  8406  facnn  12049  fac0  12050  hashresfn  12107  ruclem4  13512  fsets  14196  setsid  14211  meet0  15303  join0  15304  symgfixelsi  15933  dprd2da  16531  ply1plusgfvi  17672  uptx  19157  txcn  19158  ressxms  20059  ressms  20060  iscmet3lem3  20760  volres  20970  dvlip  21424  dvne0  21442  lhop  21447  dflog2  21971  dfrelog  21976  dvlog  22055  wilthlem2  22366  0pth  23404  2pthlem1  23429  ghsubgolem  23792  zrdivrng  23854  df1stres  25934  df2ndres  25935  ffsrn  25964  resf1o  25965  fpwrelmapffs  25969  eulerpartlemn  26694  divcnvshft  27327  divcnvlin  27328  wfrlem5  27657  frrlem5  27701  isdrngo1  28687  eldioph4b  29075  diophren  29077  seff  29520  sblpnf  29521  psgnsn  30688  bnj1326  31851