Theorem reseq2i 5126

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

Syntax hints:   = wceq 1369   |` cres 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2993  df-in 3354  df-opab 4370  df-xp 4865  df-res 4871

This theorem is referenced by:  reseq12i  5127  rescom  5154  rescnvcnv  5320  resdm2  5347  funcnvres  5506  resasplit  5600  fresaunres2  5602  fresaunres1  5603  resdif  5680  resin  5681  residpr  5905  domss2  7489  ordtypelem1  7751  ackbij2lem3  8429  facnn  12072  fac0  12073  hashresfn  12130  ruclem4  13535  fsets  14219  setsid  14234  meet0  15326  join0  15327  symgfixelsi  15959  dprd2da  16560  ply1plusgfvi  17716  uptx  19217  txcn  19218  ressxms  20119  ressms  20120  iscmet3lem3  20820  volres  21030  dvlip  21484  dvne0  21502  lhop  21507  dflog2  22031  dfrelog  22036  dvlog  22115  wilthlem2  22426  0pth  23488  2pthlem1  23513  ghsubgolem  23876  zrdivrng  23938  df1stres  26018  df2ndres  26019  ffsrn  26048  resf1o  26049  fpwrelmapffs  26053  eulerpartlemn  26783  divcnvshft  27417  divcnvlin  27418  wfrlem5  27747  frrlem5  27791  isdrngo1  28785  eldioph4b  29173  diophren  29175  seff  29618  sblpnf  29619  psgnsn  30794  bnj1326  32040