Theorem reseq2i 5920

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

Syntax hints:   = wceq 1541   ↾ cres 5613

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904  df-opab 5149  df-xp 5617  df-res 5623

This theorem is referenced by:  reseq12i  5921  rescom  5946  resdmdfsn  5975  idinxpresid  5992  rescnvcnv  6146  resdm2  6173  funcnvres  6554  resasplit  6688  fresaunres2  6690  fresaunres1  6691  resdif  6779  resin  6780  funcocnv2  6783  fvn0ssdmfun  7002  residpr  7071  eqfunressuc  7290  fprlem1  8225  domss2  9044  ordtypelem1  9399  frrlem15  9645  ackbij2lem3  10126  facnn  14177  fac0  14178  hashresfn  14242  relexpcnv  14937  divcnvshft  15757  ruclem4  16138  fsets  17075  setsid  17113  join0  18304  meet0  18305  symgfixelsi  19342  psgnsn  19427  dprd2da  19951  ply1plusgfvi  22149  uptx  23535  txcn  23536  ressxms  24435  ressms  24436  iscmet3lem3  25212  volres  25451  dvlip  25920  dvne0  25938  lhop  25943  dflog2  26491  dfrelog  26496  dvlog  26582  wilthlem2  27001  nosupbnd2lem1  27649  noinfbnd2lem1  27664  0grsubgr  29251  0pth  30097  1pthdlem1  30107  eupth2lemb  30209  ex-fpar  30434  fressupp  32661  df1stres  32677  df2ndres  32678  ffsrn  32703  resf1o  32705  fpwrelmapffs  32709  cycpmconjv  33103  sitmcl  34356  eulerpartlemn  34386  bnj1326  35030  satfv1lem  35398  divcnvlin  35769  poimirlem9  37669  zrdivrng  37993  isdrngo1  37996  ressucdifsn  38279  cnvresrn  38376  disjsuc  38797  eldioph4b  42844  diophren  42846  rclexi  43648  rtrclex  43650  cnvrcl0  43658  dfrtrcl5  43662  dfrcl2  43707  relexpiidm  43737  relexp01min  43746  relexpaddss  43751  seff  44342  sblpnf  44343  radcnvrat  44347  hashnzfzclim  44355  dvresioo  45959  fourierdlem72  46216  fourierdlem80  46224  fourierdlem94  46238  fourierdlem103  46247  fourierdlem104  46248  fourierdlem113  46257  fouriersw  46269  sge0split  46447  isubgrgrim  47960  stgr0  47991  stgr1  47992  rngcidALTV  48305  ringcidALTV  48339  tposresg  48909  tposres3  48912  tposresxp  48914