Theorem reseq2i 5996

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

Syntax hints:   = wceq 1536   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969  df-opab 5210  df-xp 5694  df-res 5700

This theorem is referenced by:  reseq12i  5997  rescom  6022  resdmdfsn  6050  idinxpresid  6067  rescnvcnv  6225  resdm2  6252  funcnvres  6645  resasplit  6778  fresaunres2  6780  fresaunres1  6781  resdif  6869  resin  6870  funcocnv2  6873  fvn0ssdmfun  7093  residpr  7162  eqfunressuc  7380  fprlem1  8323  wfrlem5OLD  8351  domss2  9174  ordtypelem1  9555  frrlem15  9794  ackbij2lem3  10277  facnn  14310  fac0  14311  hashresfn  14375  relexpcnv  15070  divcnvshft  15887  ruclem4  16266  fsets  17202  setsid  17241  join0  18462  meet0  18463  symgfixelsi  19467  psgnsn  19552  dprd2da  20076  ply1plusgfvi  22258  uptx  23648  txcn  23649  ressxms  24553  ressms  24554  iscmet3lem3  25337  volres  25576  dvlip  26046  dvne0  26064  lhop  26069  dflog2  26616  dfrelog  26621  dvlog  26707  wilthlem2  27126  nosupbnd2lem1  27774  noinfbnd2lem1  27789  0grsubgr  29309  0pth  30153  1pthdlem1  30163  eupth2lemb  30265  ex-fpar  30490  fressupp  32702  df1stres  32718  df2ndres  32719  ffsrn  32746  resf1o  32747  fpwrelmapffs  32751  cycpmconjv  33144  sitmcl  34332  eulerpartlemn  34362  bnj1326  35018  satfv1lem  35346  divcnvlin  35712  poimirlem9  37615  zrdivrng  37939  isdrngo1  37942  ressucdifsn  38225  cnvresrn  38329  disjsuc  38740  eldioph4b  42798  diophren  42800  rclexi  43604  rtrclex  43606  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  relexpiidm  43693  relexp01min  43702  relexpaddss  43707  seff  44304  sblpnf  44305  radcnvrat  44309  hashnzfzclim  44317  dvresioo  45876  fourierdlem72  46133  fourierdlem80  46141  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  fouriersw  46186  sge0split  46364  isubgrgrim  47834  stgr0  47862  stgr1  47863  rngcidALTV  48117  ringcidALTV  48151