Theorem reseq2i 5932

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 5930	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵)

Syntax hints:   = wceq 1541   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905  df-opab 5158  df-xp 5627  df-res 5633

This theorem is referenced by:  reseq12i  5933  rescom  5958  resdmdfsn  5987  idinxpresid  6004  rescnvcnv  6159  resdm2  6186  funcnvres  6567  resasplit  6701  fresaunres2  6703  fresaunres1  6704  resdif  6792  resin  6793  funcocnv2  6796  fvn0ssdmfun  7016  residpr  7085  eqfunressuc  7304  fprlem1  8239  domss2  9060  ordtypelem1  9415  frrlem15  9661  ackbij2lem3  10142  facnn  14189  fac0  14190  hashresfn  14254  relexpcnv  14949  divcnvshft  15769  ruclem4  16150  fsets  17087  setsid  17125  join0  18317  meet0  18318  symgfixelsi  19355  psgnsn  19440  dprd2da  19964  ply1plusgfvi  22173  uptx  23560  txcn  23561  ressxms  24460  ressms  24461  iscmet3lem3  25237  volres  25476  dvlip  25945  dvne0  25963  lhop  25968  dflog2  26516  dfrelog  26521  dvlog  26607  wilthlem2  27026  nosupbnd2lem1  27674  noinfbnd2lem1  27689  0grsubgr  29277  0pth  30126  1pthdlem1  30136  eupth2lemb  30238  ex-fpar  30463  fressupp  32693  df1stres  32709  df2ndres  32710  ffsrn  32735  resf1o  32737  fpwrelmapffs  32741  cycpmconjv  33152  evlextv  33635  sitmcl  34436  eulerpartlemn  34466  bnj1326  35110  satfv1lem  35478  divcnvlin  35849  poimirlem9  37742  zrdivrng  38066  isdrngo1  38069  cnvresrn  38453  dfsucmap2  38550  ressucdifsn  38573  disjsuc  38930  eldioph4b  42968  diophren  42970  rclexi  43772  rtrclex  43774  cnvrcl0  43782  dfrtrcl5  43786  dfrcl2  43831  relexpiidm  43861  relexp01min  43870  relexpaddss  43875  seff  44466  sblpnf  44467  radcnvrat  44471  hashnzfzclim  44479  dvresioo  46081  fourierdlem72  46338  fourierdlem80  46346  fourierdlem94  46360  fourierdlem103  46369  fourierdlem104  46370  fourierdlem113  46379  fouriersw  46391  sge0split  46569  isubgrgrim  48091  stgr0  48122  stgr1  48123  rngcidALTV  48436  ringcidALTV  48470  tposresg  49039  tposres3  49042  tposresxp  49044