Theorem reseq2i 5950

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

Syntax hints:   = wceq 1540   ↾ cres 5643

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924  df-opab 5173  df-xp 5647  df-res 5653

This theorem is referenced by:  reseq12i  5951  rescom  5976  resdmdfsn  6005  idinxpresid  6022  rescnvcnv  6180  resdm2  6207  funcnvres  6597  resasplit  6733  fresaunres2  6735  fresaunres1  6736  resdif  6824  resin  6825  funcocnv2  6828  fvn0ssdmfun  7049  residpr  7118  eqfunressuc  7339  fprlem1  8282  domss2  9106  ordtypelem1  9478  frrlem15  9717  ackbij2lem3  10200  facnn  14247  fac0  14248  hashresfn  14312  relexpcnv  15008  divcnvshft  15828  ruclem4  16209  fsets  17146  setsid  17184  join0  18371  meet0  18372  symgfixelsi  19372  psgnsn  19457  dprd2da  19981  ply1plusgfvi  22133  uptx  23519  txcn  23520  ressxms  24420  ressms  24421  iscmet3lem3  25197  volres  25436  dvlip  25905  dvne0  25923  lhop  25928  dflog2  26476  dfrelog  26481  dvlog  26567  wilthlem2  26986  nosupbnd2lem1  27634  noinfbnd2lem1  27649  0grsubgr  29212  0pth  30061  1pthdlem1  30071  eupth2lemb  30173  ex-fpar  30398  fressupp  32618  df1stres  32634  df2ndres  32635  ffsrn  32659  resf1o  32660  fpwrelmapffs  32664  cycpmconjv  33106  sitmcl  34349  eulerpartlemn  34379  bnj1326  35023  satfv1lem  35356  divcnvlin  35727  poimirlem9  37630  zrdivrng  37954  isdrngo1  37957  ressucdifsn  38240  cnvresrn  38337  disjsuc  38758  eldioph4b  42806  diophren  42808  rclexi  43611  rtrclex  43613  cnvrcl0  43621  dfrtrcl5  43625  dfrcl2  43670  relexpiidm  43700  relexp01min  43709  relexpaddss  43714  seff  44305  sblpnf  44306  radcnvrat  44310  hashnzfzclim  44318  dvresioo  45926  fourierdlem72  46183  fourierdlem80  46191  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  fouriersw  46236  sge0split  46414  isubgrgrim  47933  stgr0  47963  stgr1  47964  rngcidALTV  48266  ringcidALTV  48300  tposresg  48870  tposres3  48873  tposresxp  48875