Theorem reseq2i 5393

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

Syntax hints:   = wceq 1483   |` cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-opab 4713  df-xp 5120  df-res 5126

This theorem is referenced by:  reseq12i  5394  rescom  5423  resdmdfsn  5445  rescnvcnv  5597  resdm2  5624  funcnvres  5967  resasplit  6074  fresaunres2  6076  fresaunres1  6077  resdif  6157  resin  6158  funcocnv2  6161  fvn0ssdmfun  6350  residpr  6409  wfrlem5  7419  domss2  8119  ordtypelem1  8423  ackbij2lem3  9063  facnn  13062  fac0  13063  hashresfn  13128  relexpcnv  13775  divcnvshft  14587  ruclem4  14963  fsets  15891  setsid  15914  meet0  17137  join0  17138  symgfixelsi  17855  psgnsn  17940  dprd2da  18441  ply1plusgfvi  19612  uptx  21428  txcn  21429  ressxms  22330  ressms  22331  iscmet3lem3  23088  volres  23296  dvlip  23756  dvne0  23774  lhop  23779  dflog2  24307  dfrelog  24312  dvlog  24397  wilthlem2  24795  0grsubgr  26170  0pth  26986  1pthdlem1  26995  eupth2lemb  27097  df1stres  29481  df2ndres  29482  ffsrn  29504  resf1o  29505  fpwrelmapffs  29509  sitmcl  30413  eulerpartlemn  30443  bnj1326  31094  divcnvlin  31618  eqfunressuc  31660  frrlem5  31784  nosupbnd2lem1  31861  poimirlem9  33418  zrdivrng  33752  isdrngo1  33755  cnvresrn  34116  eldioph4b  37375  diophren  37377  rclexi  37922  rtrclex  37924  cnvrcl0  37932  dfrtrcl5  37936  dfrcl2  37966  relexpiidm  37996  relexp01min  38005  relexpaddss  38010  seff  38508  sblpnf  38509  radcnvrat  38513  hashnzfzclim  38521  dvresioo  40136  fourierdlem72  40395  fourierdlem80  40403  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  fouriersw  40448  sge0split  40626  rngcidALTV  41991  ringcidALTV  42054