Theorem reseq2i 5931

Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
reseq2i	⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)

Proof of Theorem reseq2i

Step	Hyp	Ref	Expression
1		reseqi.1	. 2 ⊢ 𝐴 = 𝐵
2		reseq2 5929	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)

Syntax hints:   = wceq 1540   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-opab 5158  df-xp 5629  df-res 5635

This theorem is referenced by:  reseq12i  5932  rescom  5957  resdmdfsn  5986  idinxpresid  6003  rescnvcnv  6157  resdm2  6184  funcnvres  6564  resasplit  6698  fresaunres2  6700  fresaunres1  6701  resdif  6789  resin  6790  funcocnv2  6793  fvn0ssdmfun  7012  residpr  7081  eqfunressuc  7302  fprlem1  8240  domss2  9060  ordtypelem1  9429  frrlem15  9672  ackbij2lem3  10153  facnn  14200  fac0  14201  hashresfn  14265  relexpcnv  14960  divcnvshft  15780  ruclem4  16161  fsets  17098  setsid  17136  join0  18327  meet0  18328  symgfixelsi  19332  psgnsn  19417  dprd2da  19941  ply1plusgfvi  22142  uptx  23528  txcn  23529  ressxms  24429  ressms  24430  iscmet3lem3  25206  volres  25445  dvlip  25914  dvne0  25932  lhop  25937  dflog2  26485  dfrelog  26490  dvlog  26576  wilthlem2  26995  nosupbnd2lem1  27643  noinfbnd2lem1  27658  0grsubgr  29241  0pth  30087  1pthdlem1  30097  eupth2lemb  30199  ex-fpar  30424  fressupp  32644  df1stres  32660  df2ndres  32661  ffsrn  32685  resf1o  32686  fpwrelmapffs  32690  cycpmconjv  33097  sitmcl  34321  eulerpartlemn  34351  bnj1326  34995  satfv1lem  35337  divcnvlin  35708  poimirlem9  37611  zrdivrng  37935  isdrngo1  37938  ressucdifsn  38221  cnvresrn  38318  disjsuc  38739  eldioph4b  42787  diophren  42789  rclexi  43591  rtrclex  43593  cnvrcl0  43601  dfrtrcl5  43605  dfrcl2  43650  relexpiidm  43680  relexp01min  43689  relexpaddss  43694  seff  44285  sblpnf  44286  radcnvrat  44290  hashnzfzclim  44298  dvresioo  45906  fourierdlem72  46163  fourierdlem80  46171  fourierdlem94  46185  fourierdlem103  46194  fourierdlem104  46195  fourierdlem113  46204  fouriersw  46216  sge0split  46394  isubgrgrim  47917  stgr0  47948  stgr1  47949  rngcidALTV  48262  ringcidALTV  48296  tposresg  48866  tposres3  48869  tposresxp  48871