Theorem reseq2i 5941

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

Syntax hints:   = wceq 1542   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896  df-opab 5148  df-xp 5637  df-res 5643

This theorem is referenced by:  reseq12i  5942  rescom  5967  resdmdfsn  5996  idinxpresid  6013  rescnvcnv  6168  resdm2  6195  funcnvres  6576  resasplit  6710  fresaunres2  6712  fresaunres1  6713  resdif  6801  resin  6802  funcocnv2  6805  fvn0ssdmfun  7026  residpr  7096  eqfunressuc  7316  fprlem1  8250  domss2  9074  ordtypelem1  9433  frrlem15  9681  ackbij2lem3  10162  facnn  14237  fac0  14238  hashresfn  14302  relexpcnv  14997  divcnvshft  15820  ruclem4  16201  fsets  17139  setsid  17177  join0  18369  meet0  18370  symgfixelsi  19410  psgnsn  19495  dprd2da  20019  ply1plusgfvi  22205  uptx  23590  txcn  23591  ressxms  24490  ressms  24491  iscmet3lem3  25257  volres  25495  dvlip  25960  dvne0  25978  lhop  25983  dflog2  26524  dfrelog  26529  dvlog  26615  wilthlem2  27032  nosupbnd2lem1  27679  noinfbnd2lem1  27694  0grsubgr  29347  0pth  30195  1pthdlem1  30205  eupth2lemb  30307  ex-fpar  30532  fressupp  32761  df1stres  32777  df2ndres  32778  ffsrn  32801  resf1o  32803  fpwrelmapffs  32807  cycpmconjv  33203  evlextv  33686  sitmcl  34495  eulerpartlemn  34525  bnj1326  35168  satfv1lem  35544  divcnvlin  35915  poimirlem9  37950  zrdivrng  38274  isdrngo1  38277  cnvresrn  38669  dfsucmap2  38785  ressucdifsn  38809  disjsuc  39180  eldioph4b  43239  diophren  43241  rclexi  44042  rtrclex  44044  cnvrcl0  44052  dfrtrcl5  44056  dfrcl2  44101  relexpiidm  44131  relexp01min  44140  relexpaddss  44145  seff  44736  sblpnf  44737  radcnvrat  44741  hashnzfzclim  44749  dvresioo  46349  fourierdlem72  46606  fourierdlem80  46614  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  fouriersw  46659  sge0split  46837  isubgrgrim  48405  stgr0  48436  stgr1  48437  rngcidALTV  48750  ringcidALTV  48784  tposresg  49353  tposres3  49356  tposresxp  49358