Theorem reseq2i 5270

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

Syntax hints:   = wceq 1379   |` cres 5001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-opab 4506  df-xp 5005  df-res 5011

This theorem is referenced by:  reseq12i  5271  rescom  5298  rescnvcnv  5470  resdm2  5497  funcnvres  5657  resasplit  5755  fresaunres2  5757  fresaunres1  5758  resdif  5836  resin  5837  residpr  6065  domss2  7676  ordtypelem1  7943  ackbij2lem3  8621  facnn  12323  fac0  12324  hashresfn  12381  ruclem4  13828  fsets  14516  setsid  14531  meet0  15624  join0  15625  symgfixelsi  16265  psgnsn  16351  dprd2da  16893  ply1plusgfvi  18082  uptx  19889  txcn  19890  ressxms  20791  ressms  20792  iscmet3lem3  21492  volres  21702  dvlip  22157  dvne0  22175  lhop  22180  dflog2  22704  dfrelog  22709  dvlog  22788  wilthlem2  23099  0pth  24276  2pthlem1  24301  ghsubgolem  25076  zrdivrng  25138  df1stres  27222  df2ndres  27223  ffsrn  27252  resf1o  27253  fpwrelmapffs  27257  eulerpartlemn  27988  divcnvshft  28622  divcnvlin  28623  wfrlem5  28952  frrlem5  28996  isdrngo1  29990  eldioph4b  30377  diophren  30379  seff  30820  sblpnf  30821  hashnzfzclim  30855  dvresioo  31279  fourierdlem72  31507  fourierdlem80  31515  fourierdlem94  31529  fourierdlem103  31538  fourierdlem104  31539  fourierdlem113  31548  fouriersw  31560  bnj1326  33179