Theorem reseq2i 5947

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

Syntax hints:   = wceq 1540   ↾ cres 5640

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921  df-opab 5170  df-xp 5644  df-res 5650

This theorem is referenced by:  reseq12i  5948  rescom  5973  resdmdfsn  6002  idinxpresid  6019  rescnvcnv  6177  resdm2  6204  funcnvres  6594  resasplit  6730  fresaunres2  6732  fresaunres1  6733  resdif  6821  resin  6822  funcocnv2  6825  fvn0ssdmfun  7046  residpr  7115  eqfunressuc  7336  fprlem1  8279  domss2  9100  ordtypelem1  9471  frrlem15  9710  ackbij2lem3  10193  facnn  14240  fac0  14241  hashresfn  14305  relexpcnv  15001  divcnvshft  15821  ruclem4  16202  fsets  17139  setsid  17177  join0  18364  meet0  18365  symgfixelsi  19365  psgnsn  19450  dprd2da  19974  ply1plusgfvi  22126  uptx  23512  txcn  23513  ressxms  24413  ressms  24414  iscmet3lem3  25190  volres  25429  dvlip  25898  dvne0  25916  lhop  25921  dflog2  26469  dfrelog  26474  dvlog  26560  wilthlem2  26979  nosupbnd2lem1  27627  noinfbnd2lem1  27642  0grsubgr  29205  0pth  30054  1pthdlem1  30064  eupth2lemb  30166  ex-fpar  30391  fressupp  32611  df1stres  32627  df2ndres  32628  ffsrn  32652  resf1o  32653  fpwrelmapffs  32657  cycpmconjv  33099  sitmcl  34342  eulerpartlemn  34372  bnj1326  35016  satfv1lem  35349  divcnvlin  35720  poimirlem9  37623  zrdivrng  37947  isdrngo1  37950  ressucdifsn  38233  cnvresrn  38330  disjsuc  38751  eldioph4b  42799  diophren  42801  rclexi  43604  rtrclex  43606  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  relexpiidm  43693  relexp01min  43702  relexpaddss  43707  seff  44298  sblpnf  44299  radcnvrat  44303  hashnzfzclim  44311  dvresioo  45919  fourierdlem72  46176  fourierdlem80  46184  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  fouriersw  46229  sge0split  46407  isubgrgrim  47929  stgr0  47959  stgr1  47960  rngcidALTV  48262  ringcidALTV  48296  tposresg  48866  tposres3  48869  tposresxp  48871