Theorem reseq2i 5259

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

Syntax hints:   = wceq 1398   |` cres 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-opab 4498  df-xp 4994  df-res 5000

This theorem is referenced by:  reseq12i  5260  rescom  5286  rescnvcnv  5453  resdm2  5480  funcnvres  5639  resasplit  5737  fresaunres2  5739  fresaunres1  5740  resdif  5818  resin  5819  fvn0ssdmfun  5998  residpr  6051  domss2  7669  ordtypelem1  7935  ackbij2lem3  8612  facnn  12337  fac0  12338  hashresfn  12395  relexpcnv  12950  ruclem4  14051  fsets  14744  setsid  14759  meet0  15966  join0  15967  symgfixelsi  16659  psgnsn  16744  dprd2da  17286  ply1plusgfvi  18478  uptx  20292  txcn  20293  ressxms  21194  ressms  21195  iscmet3lem3  21895  volres  22105  dvlip  22560  dvne0  22578  lhop  22583  dflog2  23114  dfrelog  23119  dvlog  23200  wilthlem2  23541  0pth  24774  2pthlem1  24799  ghsubgolemOLD  25570  zrdivrng  25632  df1stres  27750  df2ndres  27751  ffsrn  27783  resf1o  27784  fpwrelmapffs  27788  eulerpartlemn  28584  divcnvshft  29358  divcnvlin  29359  wfrlem5  29587  frrlem5  29631  isdrngo1  30599  eldioph4b  30984  diophren  30986  seff  31430  sblpnf  31431  radcnvrat  31436  hashnzfzclim  31468  dvresioo  31957  fourierdlem72  32200  fourierdlem80  32208  fourierdlem94  32222  fourierdlem103  32231  fourierdlem104  32232  fourierdlem113  32241  fouriersw  32253  rngcidALTV  33053  ringcidALTV  33116  bnj1326  34483  dfrcl2  38193  relexpaddss  38205  relexp01min  38219  relexpiidm  38222