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 1542   ↾ cres 5626

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 3391  df-in 3897  df-opab 5149  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  7020  residpr  7090  eqfunressuc  7309  fprlem1  8243  domss2  9067  ordtypelem1  9426  frrlem15  9672  ackbij2lem3  10153  facnn  14228  fac0  14229  hashresfn  14293  relexpcnv  14988  divcnvshft  15811  ruclem4  16192  fsets  17130  setsid  17168  join0  18360  meet0  18361  symgfixelsi  19401  psgnsn  19486  dprd2da  20010  ply1plusgfvi  22215  uptx  23600  txcn  23601  ressxms  24500  ressms  24501  iscmet3lem3  25267  volres  25505  dvlip  25970  dvne0  25988  lhop  25993  dflog2  26537  dfrelog  26542  dvlog  26628  wilthlem2  27046  nosupbnd2lem1  27693  noinfbnd2lem1  27708  0grsubgr  29361  0pth  30210  1pthdlem1  30220  eupth2lemb  30322  ex-fpar  30547  fressupp  32776  df1stres  32792  df2ndres  32793  ffsrn  32816  resf1o  32818  fpwrelmapffs  32822  cycpmconjv  33218  evlextv  33701  sitmcl  34511  eulerpartlemn  34541  bnj1326  35184  satfv1lem  35560  divcnvlin  35931  poimirlem9  37964  zrdivrng  38288  isdrngo1  38291  cnvresrn  38683  dfsucmap2  38799  ressucdifsn  38823  disjsuc  39194  eldioph4b  43257  diophren  43259  rclexi  44060  rtrclex  44062  cnvrcl0  44070  dfrtrcl5  44074  dfrcl2  44119  relexpiidm  44149  relexp01min  44158  relexpaddss  44163  seff  44754  sblpnf  44755  radcnvrat  44759  hashnzfzclim  44767  dvresioo  46367  fourierdlem72  46624  fourierdlem80  46632  fourierdlem94  46646  fourierdlem103  46655  fourierdlem104  46656  fourierdlem113  46665  fouriersw  46677  sge0split  46855  isubgrgrim  48417  stgr0  48448  stgr1  48449  rngcidALTV  48762  ringcidALTV  48796  tposresg  49365  tposres3  49368  tposresxp  49370