Theorem reseq2i 5113

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

Syntax hints:   = wceq 1437   |` cres 4847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-in 3440  df-opab 4476  df-xp 4851  df-res 4857

This theorem is referenced by:  reseq12i  5114  rescom  5140  rescnvcnv  5309  resdm2  5336  funcnvres  5661  resasplit  5761  fresaunres2  5763  fresaunres1  5764  resdif  5842  resin  5843  fvn0ssdmfun  6019  residpr  6074  wfrlem5  7039  domss2  7728  ordtypelem1  8024  ackbij2lem3  8660  facnn  12447  fac0  12448  hashresfn  12509  relexpcnv  13066  divcnvshft  13880  ruclem4  14253  fsets  15101  setsid  15116  meet0  16327  join0  16328  symgfixelsi  17020  psgnsn  17105  dprd2da  17603  ply1plusgfvi  18763  uptx  20564  txcn  20565  ressxms  21464  ressms  21465  iscmet3lem3  22146  volres  22356  dvlip  22819  dvne0  22837  lhop  22842  dflog2  23372  dfrelog  23377  dvlog  23458  wilthlem2  23856  0pth  25142  2pthlem1  25167  ghsubgolemOLD  25940  zrdivrng  26002  df1stres  28121  df2ndres  28122  ffsrn  28154  resf1o  28155  fpwrelmapffs  28159  eulerpartlemn  29037  bnj1326  29620  divcnvlin  30151  frrlem5  30302  poimirlem9  31653  isdrngo1  31899  eldioph4b  35363  diophren  35365  dfrcl2  35909  relexpiidm  35939  relexp01min  35948  relexpaddss  35953  seff  36298  sblpnf  36299  radcnvrat  36304  hashnzfzclim  36312  dvresioo  37369  fourierdlem72  37614  fourierdlem80  37622  fourierdlem94  37636  fourierdlem103  37645  fourierdlem104  37646  fourierdlem113  37655  fouriersw  37667  sge0split  37789  rngcidALTV  38764  ringcidALTV  38827