Theorem reseq2i 5943

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

Syntax hints:   = wceq 1542   ↾ cres 5634

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910  df-opab 5163  df-xp 5638  df-res 5644

This theorem is referenced by:  reseq12i  5944  rescom  5969  resdmdfsn  5998  idinxpresid  6015  rescnvcnv  6170  resdm2  6197  funcnvres  6578  resasplit  6712  fresaunres2  6714  fresaunres1  6715  resdif  6803  resin  6804  funcocnv2  6807  fvn0ssdmfun  7028  residpr  7098  eqfunressuc  7317  fprlem1  8252  domss2  9076  ordtypelem1  9435  frrlem15  9681  ackbij2lem3  10162  facnn  14210  fac0  14211  hashresfn  14275  relexpcnv  14970  divcnvshft  15790  ruclem4  16171  fsets  17108  setsid  17146  join0  18338  meet0  18339  symgfixelsi  19376  psgnsn  19461  dprd2da  19985  ply1plusgfvi  22194  uptx  23581  txcn  23582  ressxms  24481  ressms  24482  iscmet3lem3  25258  volres  25497  dvlip  25966  dvne0  25984  lhop  25989  dflog2  26537  dfrelog  26542  dvlog  26628  wilthlem2  27047  nosupbnd2lem1  27695  noinfbnd2lem1  27710  0grsubgr  29363  0pth  30212  1pthdlem1  30222  eupth2lemb  30324  ex-fpar  30549  fressupp  32777  df1stres  32793  df2ndres  32794  ffsrn  32817  resf1o  32819  fpwrelmapffs  32823  cycpmconjv  33235  evlextv  33718  sitmcl  34528  eulerpartlemn  34558  bnj1326  35201  satfv1lem  35575  divcnvlin  35946  poimirlem9  37877  zrdivrng  38201  isdrngo1  38204  cnvresrn  38596  dfsucmap2  38712  ressucdifsn  38736  disjsuc  39107  eldioph4b  43165  diophren  43167  rclexi  43968  rtrclex  43970  cnvrcl0  43978  dfrtrcl5  43982  dfrcl2  44027  relexpiidm  44057  relexp01min  44066  relexpaddss  44071  seff  44662  sblpnf  44663  radcnvrat  44667  hashnzfzclim  44675  dvresioo  46276  fourierdlem72  46533  fourierdlem80  46541  fourierdlem94  46555  fourierdlem103  46564  fourierdlem104  46565  fourierdlem113  46574  fouriersw  46586  sge0split  46764  isubgrgrim  48286  stgr0  48317  stgr1  48318  rngcidALTV  48631  ringcidALTV  48665  tposresg  49234  tposres3  49237  tposresxp  49239