Theorem reseq2i 5692

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

Syntax hints:   = wceq 1507   ↾ cres 5409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097  df-v 3417  df-in 3836  df-opab 4992  df-xp 5413  df-res 5419

This theorem is referenced by:  reseq12i  5693  rescom  5724  resdmdfsn  5746  rescnvcnv  5900  resdm2  5927  funcnvres  6265  resasplit  6377  fresaunres2  6379  fresaunres1  6380  resdif  6464  resin  6465  funcocnv2  6468  fvn0ssdmfun  6667  residpr  6728  wfrlem5  7763  domss2  8472  ordtypelem1  8777  ackbij2lem3  9461  facnn  13450  fac0  13451  hashresfn  13515  relexpcnv  14255  divcnvshft  15070  ruclem4  15447  fsets  16372  setsid  16394  meet0  17605  join0  17606  symgfixelsi  18324  psgnsn  18410  dprd2da  18914  ply1plusgfvi  20113  uptx  21937  txcn  21938  ressxms  22838  ressms  22839  iscmet3lem3  23596  volres  23832  dvlip  24293  dvne0  24311  lhop  24316  dflog2  24845  dfrelog  24850  dvlog  24935  wilthlem2  25348  0grsubgr  26763  0pth  27654  1pthdlem1  27664  eupth2lemb  27767  df1stres  30198  df2ndres  30199  ffsrn  30224  resf1o  30225  fpwrelmapffs  30229  sitmcl  31260  eulerpartlemn  31290  bnj1326  31949  divcnvlin  32490  eqfunressuc  32531  fprlem1  32664  frrlem15  32669  nosupbnd2lem1  32742  poimirlem9  34348  zrdivrng  34679  isdrngo1  34682  cnvresrn  35057  eldioph4b  38810  diophren  38812  rclexi  39344  rtrclex  39346  cnvrcl0  39354  dfrtrcl5  39358  dfrcl2  39388  relexpiidm  39418  relexp01min  39427  relexpaddss  39432  seff  40063  sblpnf  40064  radcnvrat  40068  hashnzfzclim  40076  dvresioo  41642  fourierdlem72  41900  fourierdlem80  41908  fourierdlem94  41922  fourierdlem103  41931  fourierdlem104  41932  fourierdlem113  41941  fouriersw  41953  sge0split  42128  rngcidALTV  43632  ringcidALTV  43695