Theorem reseq2i 5102

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

Syntax hints:   = wceq 1444   |` cres 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-opab 4462  df-xp 4840  df-res 4846

This theorem is referenced by:  reseq12i  5103  rescom  5129  rescnvcnv  5298  resdm2  5325  funcnvres  5652  resasplit  5753  fresaunres2  5755  fresaunres1  5756  resdif  5834  resin  5835  fvn0ssdmfun  6013  residpr  6068  wfrlem5  7040  domss2  7731  ordtypelem1  8033  ackbij2lem3  8671  facnn  12461  fac0  12462  hashresfn  12523  relexpcnv  13098  divcnvshft  13913  ruclem4  14286  fsets  15149  setsid  15164  meet0  16383  join0  16384  symgfixelsi  17076  psgnsn  17161  dprd2da  17675  ply1plusgfvi  18835  uptx  20640  txcn  20641  ressxms  21540  ressms  21541  iscmet3lem3  22260  volres  22482  dvlip  22945  dvne0  22963  lhop  22968  dflog2  23510  dfrelog  23515  dvlog  23596  wilthlem2  23994  0pth  25300  2pthlem1  25325  ghsubgolemOLD  26098  zrdivrng  26160  df1stres  28284  df2ndres  28285  ffsrn  28314  resf1o  28315  fpwrelmapffs  28319  sitmcl  29184  eulerpartlemn  29214  bnj1326  29835  divcnvlin  30367  frrlem5  30518  poimirlem9  31949  isdrngo1  32195  eldioph4b  35654  diophren  35656  rclexi  36222  rtrclex  36224  cnvrcl0  36232  dfrtrcl5  36236  dfrcl2  36266  relexpiidm  36296  relexp01min  36305  relexpaddss  36310  seff  36657  sblpnf  36658  radcnvrat  36663  hashnzfzclim  36671  dvresioo  37793  fourierdlem72  38042  fourierdlem80  38050  fourierdlem94  38064  fourierdlem103  38073  fourierdlem104  38074  fourierdlem113  38083  fouriersw  38095  sge0split  38251  0grsubgr  39350  rngcidALTV  40046  ringcidALTV  40109