Theorem reseq2i 5994

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

Syntax hints:   = wceq 1540   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-opab 5206  df-xp 5691  df-res 5697

This theorem is referenced by:  reseq12i  5995  rescom  6020  resdmdfsn  6049  idinxpresid  6066  rescnvcnv  6224  resdm2  6251  funcnvres  6644  resasplit  6778  fresaunres2  6780  fresaunres1  6781  resdif  6869  resin  6870  funcocnv2  6873  fvn0ssdmfun  7094  residpr  7163  eqfunressuc  7381  fprlem1  8325  wfrlem5OLD  8353  domss2  9176  ordtypelem1  9558  frrlem15  9797  ackbij2lem3  10280  facnn  14314  fac0  14315  hashresfn  14379  relexpcnv  15074  divcnvshft  15891  ruclem4  16270  fsets  17206  setsid  17244  join0  18450  meet0  18451  symgfixelsi  19453  psgnsn  19538  dprd2da  20062  ply1plusgfvi  22243  uptx  23633  txcn  23634  ressxms  24538  ressms  24539  iscmet3lem3  25324  volres  25563  dvlip  26032  dvne0  26050  lhop  26055  dflog2  26602  dfrelog  26607  dvlog  26693  wilthlem2  27112  nosupbnd2lem1  27760  noinfbnd2lem1  27775  0grsubgr  29295  0pth  30144  1pthdlem1  30154  eupth2lemb  30256  ex-fpar  30481  fressupp  32697  df1stres  32713  df2ndres  32714  ffsrn  32740  resf1o  32741  fpwrelmapffs  32745  cycpmconjv  33162  sitmcl  34353  eulerpartlemn  34383  bnj1326  35040  satfv1lem  35367  divcnvlin  35733  poimirlem9  37636  zrdivrng  37960  isdrngo1  37963  ressucdifsn  38246  cnvresrn  38349  disjsuc  38760  eldioph4b  42822  diophren  42824  rclexi  43628  rtrclex  43630  cnvrcl0  43638  dfrtrcl5  43642  dfrcl2  43687  relexpiidm  43717  relexp01min  43726  relexpaddss  43731  seff  44328  sblpnf  44329  radcnvrat  44333  hashnzfzclim  44341  dvresioo  45936  fourierdlem72  46193  fourierdlem80  46201  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  fouriersw  46246  sge0split  46424  isubgrgrim  47897  stgr0  47927  stgr1  47928  rngcidALTV  48190  ringcidALTV  48224  tposresg  48778  tposres3  48781  tposresxp  48783