Theorem reseq2d 5999

Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
reseqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
reseq2d	⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Proof of Theorem reseq2d

Step	Hyp	Ref	Expression
1		reseqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		reseq2 5994	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1536   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969  df-opab 5210  df-xp 5694  df-res 5700

This theorem is referenced by:  reseq12d  6000  resresdm  6254  relresfld  6297  fnunres1  6680  f1orescnv  6863  fococnv2  6874  fvn0ssdmfun  7093  fnressn  7177  fnsnsplit  7203  oprssov  7601  curry1  8127  curry2  8130  dftpos2  8266  frecseq123  8305  fpr3g  8308  frrlem1  8309  frrlem4  8312  frrlem12  8320  fpr2a  8325  wrecseq123OLD  8338  wfr3g  8345  wfrlem1OLD  8346  wfrlem4OLD  8350  wfrlem14OLD  8360  wfr2aOLD  8364  dfrecs3  8410  dfrecs3OLD  8411  tfrlem16  8431  tfr2ALT  8439  tfr3ALT  8440  on2recsov  8704  sbthlem4  9124  mapunen  9184  hartogslem1  9579  frr3g  9793  frr2  9797  axdc3lem2  10488  fseq1p1m1  13634  resunimafz0  14480  hashf1lem1  14490  relexp0g  15057  relexp0  15058  relexpsucnnr  15060  dfrtrcl2  15097  bpolylem  16080  setsval  17200  idfuval  17926  idfu2nd  17927  resf1st  17944  idfusubc0  17949  idfusubc  17950  setcid  18139  catcisolem  18163  estrcid  18188  funcestrcsetclem5  18199  funcsetcestrclem5  18214  funcsetcestrclem7  18216  1stfval  18246  1stf2  18248  2ndfval  18249  2ndf2  18251  1stfcl  18252  2ndfcl  18253  curf2ndf  18303  hofcl  18315  isps  18625  cnvps  18635  isdir  18655  dirref  18658  tsrdir  18661  frmdval  18876  frmdplusg  18879  gsum2dlem2  20003  dprd2da  20076  dpjval  20090  ablfac1eulem  20106  ablfac1eu  20107  rngcval  20634  rnghmsubcsetclem1  20647  rngccat  20650  rngcid  20651  rngcifuestrc  20655  funcrngcsetc  20656  funcrngcsetcALT  20657  ringcval  20663  rhmsubcsetclem1  20676  ringccat  20679  ringcid  20680  rhmsubcrngclem1  20682  rhmsubcrngc  20684  funcringcsetc  20690  rhmsubc  20705  psrplusg  21973  opsrtoslem2  22097  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  imacmp  23420  ptuncnv  23830  tgphaus  24140  tsmsres  24167  tsmsxplem1  24176  tsmsxplem2  24177  trust  24253  metreslem  24387  imasdsf1olem  24398  xmspropd  24498  mspropd  24499  imasf1oxms  24517  imasf1oms  24518  nmpropd2  24623  isngp2  24625  ngppropd  24665  tngngp2  24688  cphsscph  25298  cmspropd  25396  cmssmscld  25397  mbfres2  25693  limciun  25943  dvmptres3  26008  dvmptres2  26014  dvmptntr  26023  dvlipcn  26047  dvlip2  26048  c1liplem1  26049  dvgt0lem1  26055  lhop1lem  26066  dvcnvrelem1  26070  dvcvx  26073  ftc2ditglem  26100  wilthlem2  27126  dchrval  27292  dchrelbas2  27295  noresle  27756  nosupcbv  27761  nosupno  27762  nosupdm  27763  nosupfv  27765  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd1  27773  nosupbnd2  27775  noinfcbv  27776  noinfno  27777  noinfdm  27778  noinffv  27780  noinfres  27781  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd1  27788  noinfbnd2  27790  noetalem1  27800  norecov  27994  norec2ov  28004  egrsubgr  29308  pthdlem1  29798  eupthvdres  30263  eupth2lem3  30264  eupth2  30267  eucrct2eupth  30273  hhssablo  31291  hhssnvt  31293  hhsssh  31297  fressupp  32702  resf1o  32747  gsummpt2d  33034  gsumpart  33042  symgcom  33085  tocycval  33110  tocycfv  33111  tocycf  33119  tocyc01  33120  cycpm2tr  33121  cycpmconjslem1  33156  cycpmconjslem2  33157  nsgqusf1o  33423  qtophaus  33796  esumcvg  34066  eulerpartlemn  34362  sseqp1  34376  signsvtn0  34563  ftc2re  34591  reprsuc  34608  bnj1385  34824  bnj1326  35018  bnj1321  35019  bnj1442  35041  bnj1450  35042  bnj1463  35047  bnj1529  35062  f1resfz0f1d  35097  pfxwlk  35107  pthhashvtx  35111  cvmliftlem5  35273  cvmliftlem7  35275  cvmliftlem10  35278  cvmliftlem11  35279  cvmliftlem15  35282  cvmlift2lem11  35297  cvmlift2lem12  35298  satffunlem1lem1  35386  satffunlem2lem1  35388  eldm3  35740  funsseq  35748  finixpnum  37591  poimirlem3  37609  poimirlem4  37610  poimirlem9  37615  sdclem2  37728  prdsbnd2  37781  isdivrngo  37936  drngoi  37937  elrefsymrels2  38550  eleqvrels2  38573  dibffval  41122  hdmapffval  41808  hdmapfval  41809  eqresfnbd  42251  dvun  42367  eldiophb  42744  diophrw  42746  diophin  42759  tfsconcatrev  43337  ofoafg  43343  resisoeq45d  43409  rclexi  43604  rtrclex  43606  rtrclexi  43610  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  fvmptiunrelexplb0da  43674  sblpnf  44305  fresin2  45114  limsupresuz  45658  limsupvaluz  45663  limsupvaluz2  45693  supcnvlimsup  45695  climrescn  45703  liminfresuz  45739  cncfuni  45841  dvresntr  45873  dvbdfbdioolem1  45883  itgiccshift  45935  itgperiod  45936  dirkercncflem2  46059  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem58  46119  fourierdlem72  46133  fourierdlem74  46135  fourierdlem75  46136  fourierdlem81  46142  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fouriersw  46186  voncmpl  46576  funcoressn  46991  funressnmo  46995  f1cof1blem  47023  funfocofob  47027  funressndmafv2rn  47172  f1oresf1orab  47238  isubgrgrim  47834  stgrfv  47855  gpgov  47936  rngcidALTV  48117  rhmsubcALTVlem3  48126  funcringcsetcALTV2lem5  48137  ringcidALTV  48151  funcringcsetclem5ALTV  48160  itcoval  48510  itcoval0mpt  48515  itcovalendof  48518  aacllem  49031