Theorem reseq2i 5958

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

Syntax hints:   = wceq 1559   ↾ cres 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3909  df-opab 5160  df-xp 5649  df-res 5655

This theorem is referenced by:  reseq12i  5959  rescom  5984  resindm  6012  resdmdfsn  6014  resdmdfsnOLD  6015  idinxpresid  6033  rescnvcnv  6186  resdm2  6213  funcnvres  6594  resasplit  6729  fresaunres2  6731  fresaunres1  6732  resdif  6823  resin  6824  funcocnv2  6827  fvn0ssdmfun  7050  residpr  7120  eqfunressuc  7340  fprlem1  8275  domss2  9102  ordtypelem1  9460  frrlem15  9709  ackbij2lem3  10190  facnn  14282  fac0  14283  hashresfn  14347  relexpcnv  15042  divcnvshft  15876  ruclem4  16257  fsets  17196  setsid  17234  join0  18426  meet0  18427  symgfixelsi  19466  psgnsn  19551  dprd2da  20075  ply1plusgfvi  22291  uptx  23673  txcn  23674  ressxms  24573  ressms  24574  iscmet3lem3  25340  volres  25578  dvlip  26043  dvne0  26061  lhop  26066  dflog2  26613  dfrelog  26618  dvlog  26704  wilthlem2  27121  nosupbnd2lem1  27767  noinfbnd2lem1  27782  0grsubgr  29436  0pth  30284  1pthdlem1  30294  eupth2lemb  30396  ex-fpar  30621  fressupp  32851  df1stres  32867  df2ndres  32868  ffsrn  32891  resf1o  32893  fpwrelmapffs  32897  cycpmconjv  33283  evlextv  33800  sitmcl  34609  eulerpartlemn  34639  bnj1326  35282  satfv1lem  35673  divcnvlin  36044  poimirlem9  38089  zrdivrng  38413  isdrngo1  38416  cnvresrn  38808  dfsucmap2  38924  ressucdifsn  38948  disjsuc  39319  eldioph4b  43349  diophren  43351  rclexi  44152  rtrclex  44154  cnvrcl0  44162  dfrtrcl5  44166  dfrcl2  44211  relexpiidm  44241  relexp01min  44250  relexpaddss  44255  seff  44846  sblpnf  44847  radcnvrat  44851  hashnzfzclim  44859  dvresioo  46456  fourierdlem72  46713  fourierdlem80  46721  fourierdlem94  46735  fourierdlem103  46744  fourierdlem104  46745  fourierdlem113  46754  fouriersw  46766  sge0split  46944  isubgrgrim  48512  stgr0  48543  stgr1  48544  rngcidALTV  48857  ringcidALTV  48891  tposresg  49460  tposres3  49463  tposresxp  49465