Theorem reseq2i 5108

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

Syntax hints:   = wceq 1452   |` cres 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-opab 4455  df-xp 4845  df-res 4851

This theorem is referenced by:  reseq12i  5109  rescom  5135  rescnvcnv  5305  resdm2  5332  funcnvres  5662  resasplit  5765  fresaunres2  5767  fresaunres1  5768  resdif  5848  resin  5849  fvn0ssdmfun  6028  residpr  6084  wfrlem5  7058  domss2  7749  ordtypelem1  8051  ackbij2lem3  8689  facnn  12499  fac0  12500  hashresfn  12561  relexpcnv  13175  divcnvshft  13990  ruclem4  14363  fsets  15227  setsid  15242  meet0  16461  join0  16462  symgfixelsi  17154  psgnsn  17239  dprd2da  17753  ply1plusgfvi  18912  uptx  20717  txcn  20718  ressxms  21618  ressms  21619  iscmet3lem3  22338  volres  22560  dvlip  23024  dvne0  23042  lhop  23047  dflog2  23589  dfrelog  23594  dvlog  23675  wilthlem2  24073  0pth  25379  2pthlem1  25404  ghsubgolemOLD  26179  zrdivrng  26241  df1stres  28359  df2ndres  28360  ffsrn  28389  resf1o  28390  fpwrelmapffs  28394  sitmcl  29257  eulerpartlemn  29287  bnj1326  29907  divcnvlin  30438  frrlem5  30589  poimirlem9  32013  isdrngo1  32259  eldioph4b  35725  diophren  35727  rclexi  36293  rtrclex  36295  cnvrcl0  36303  dfrtrcl5  36307  dfrcl2  36337  relexpiidm  36367  relexp01min  36376  relexpaddss  36381  seff  36727  sblpnf  36728  radcnvrat  36733  hashnzfzclim  36741  dvresioo  37890  fourierdlem72  38154  fourierdlem80  38162  fourierdlem94  38176  fourierdlem103  38185  fourierdlem104  38186  fourierdlem113  38195  fouriersw  38207  sge0split  38365  0grsubgr  39514  0pth-av  40014  1pthdlem1  40023  eupth2lemb  40149  rngcidALTV  40501  ringcidALTV  40564