Theorem reseq2i 5935

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

Syntax hints:   = wceq 1541   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-opab 5161  df-xp 5630  df-res 5636

This theorem is referenced by:  reseq12i  5936  rescom  5961  resdmdfsn  5990  idinxpresid  6007  rescnvcnv  6162  resdm2  6189  funcnvres  6570  resasplit  6704  fresaunres2  6706  fresaunres1  6707  resdif  6795  resin  6796  funcocnv2  6799  fvn0ssdmfun  7019  residpr  7088  eqfunressuc  7307  fprlem1  8242  domss2  9064  ordtypelem1  9423  frrlem15  9669  ackbij2lem3  10150  facnn  14198  fac0  14199  hashresfn  14263  relexpcnv  14958  divcnvshft  15778  ruclem4  16159  fsets  17096  setsid  17134  join0  18326  meet0  18327  symgfixelsi  19364  psgnsn  19449  dprd2da  19973  ply1plusgfvi  22182  uptx  23569  txcn  23570  ressxms  24469  ressms  24470  iscmet3lem3  25246  volres  25485  dvlip  25954  dvne0  25972  lhop  25977  dflog2  26525  dfrelog  26530  dvlog  26616  wilthlem2  27035  nosupbnd2lem1  27683  noinfbnd2lem1  27698  0grsubgr  29351  0pth  30200  1pthdlem1  30210  eupth2lemb  30312  ex-fpar  30537  fressupp  32767  df1stres  32783  df2ndres  32784  ffsrn  32807  resf1o  32809  fpwrelmapffs  32813  cycpmconjv  33224  evlextv  33707  sitmcl  34508  eulerpartlemn  34538  bnj1326  35182  satfv1lem  35556  divcnvlin  35927  poimirlem9  37830  zrdivrng  38154  isdrngo1  38157  cnvresrn  38541  dfsucmap2  38638  ressucdifsn  38661  disjsuc  39018  eldioph4b  43053  diophren  43055  rclexi  43856  rtrclex  43858  cnvrcl0  43866  dfrtrcl5  43870  dfrcl2  43915  relexpiidm  43945  relexp01min  43954  relexpaddss  43959  seff  44550  sblpnf  44551  radcnvrat  44555  hashnzfzclim  44563  dvresioo  46165  fourierdlem72  46422  fourierdlem80  46430  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem113  46463  fouriersw  46475  sge0split  46653  isubgrgrim  48175  stgr0  48206  stgr1  48207  rngcidALTV  48520  ringcidALTV  48554  tposresg  49123  tposres3  49126  tposresxp  49128