Theorem reseq2i 5977

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

Syntax hints:   = wceq 1570   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913  df-opab 5175  df-xp 5669  df-res 5675

This theorem is referenced by:  reseq12i  5978  rescom  6003  resindm  6031  resdmdfsn  6033  resdmdfsnOLD  6034  idinxpresid  6052  imadifssran  6204  rescnvcnv  6207  resdm2  6234  funcnvres  6616  resasplit  6750  fresaunres2  6752  fresaunres1  6753  resdif  6844  resin  6845  funcocnv2  6848  fvn0ssdmfun  7071  residpr  7141  eqfunressuc  7361  fprlem1  8298  domss2  9125  ordtypelem1  9481  frrlem15  9730  ackbij2lem3  10224  facnn  14313  fac0  14314  hashresfn  14378  relexpcnv  15074  divcnvshft  15911  ruclem4  16291  fsets  17230  setsid  17268  join0  18460  meet0  18461  symgfixelsi  19506  psgnsn  19591  dprd2da  20115  ply1plusgfvi  22382  uptx  23763  txcn  23764  ressxms  24663  ressms  24664  iscmet3lem3  25430  volres  25668  dvlip  26133  dvne0  26151  lhop  26156  dflog2  26706  dfrelog  26711  dvlog  26797  wilthlem2  27214  nosupbnd2lem1  27860  noinfbnd2lem1  27875  0grsubgr  29609  0pth  30457  1pthdlem1  30467  eupth2lemb  30569  ex-fpar  30794  fressupp  33014  df1stres  33030  df2ndres  33031  ffsrn  33054  resf1o  33056  fpwrelmapffs  33060  cycpmconjv  33443  evlextv  33913  sitmcl  34722  eulerpartlemn  34752  bnj1326  35395  satfv1lem  35835  divcnvlin  36206  poimirlem9  38261  zrdivrng  38585  isdrngo1  38588  cnvresrn  38978  dfsucmap2  39094  ressucdifsn  39118  disjsuc  39489  eldioph4b  43521  diophren  43523  rclexi  44324  rtrclex  44326  cnvrcl0  44334  dfrtrcl5  44338  dfrcl2  44383  relexpiidm  44413  relexp01min  44422  relexpaddss  44427  seff  45002  sblpnf  45003  radcnvrat  45007  hashnzfzclim  45015  dvresioo  46618  fourierdlem72  46875  fourierdlem80  46883  fourierdlem94  46897  fourierdlem103  46906  fourierdlem104  46907  fourierdlem113  46916  fouriersw  46928  sge0split  47106  isubgrgrim  48677  stgr0  48708  stgr1  48709  rngcidALTV  49022  ringcidALTV  49056  tposresg  49639  tposres3  49642  tposresxp  49644