Theorem reseq2d 5938

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 5933	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5626

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-opab 5161  df-xp 5630  df-res 5636

This theorem is referenced by:  reseq12d  5939  imadifssran  6109  resresdm  6191  relresfld  6234  fnunres1  6604  f1orescnv  6789  fococnv2  6800  fvn0ssdmfun  7019  fnressn  7103  fnsnsplit  7130  oprssov  7527  curry1  8046  curry2  8049  dftpos2  8185  frecseq123  8224  fpr3g  8227  frrlem1  8228  frrlem4  8231  frrlem12  8239  fpr2a  8244  wfr3g  8261  dfrecs3  8304  tfrlem16  8324  tfr2ALT  8332  tfr3ALT  8333  on2recsov  8596  sbthlem4  9018  mapunen  9074  hartogslem1  9447  frr3g  9668  frr2  9672  axdc3lem2  10361  fseq1p1m1  13514  resunimafz0  14368  hashf1lem1  14378  relexp0g  14945  relexp0  14946  relexpsucnnr  14948  dfrtrcl2  14985  bpolylem  15971  setsval  17094  idfuval  17800  idfu2nd  17801  resf1st  17818  idfusubc0  17823  idfusubc  17824  setcid  18010  catcisolem  18034  estrcid  18057  funcestrcsetclem5  18067  funcsetcestrclem5  18082  funcsetcestrclem7  18084  1stfval  18114  1stf2  18116  2ndfval  18117  2ndf2  18119  1stfcl  18120  2ndfcl  18121  curf2ndf  18170  hofcl  18182  isps  18491  cnvps  18501  isdir  18521  dirref  18524  tsrdir  18527  frmdval  18776  frmdplusg  18779  gsum2dlem2  19900  dprd2da  19973  dpjval  19987  ablfac1eulem  20003  ablfac1eu  20004  rngcval  20551  rnghmsubcsetclem1  20564  rngccat  20567  rngcid  20568  rngcifuestrc  20572  funcrngcsetc  20573  funcrngcsetcALT  20574  ringcval  20580  rhmsubcsetclem1  20593  ringccat  20596  ringcid  20597  rhmsubcrngclem1  20599  rhmsubcrngc  20601  funcringcsetc  20607  rhmsubc  20622  psrplusg  21892  opsrtoslem2  22011  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  imacmp  23341  ptuncnv  23751  tgphaus  24061  tsmsres  24088  tsmsxplem1  24097  tsmsxplem2  24098  trust  24173  metreslem  24306  imasdsf1olem  24317  xmspropd  24417  mspropd  24418  imasf1oxms  24433  imasf1oms  24434  nmpropd2  24539  isngp2  24541  ngppropd  24581  tngngp2  24596  cphsscph  25207  cmspropd  25305  cmssmscld  25306  mbfres2  25602  limciun  25851  dvmptres3  25916  dvmptres2  25922  dvmptntr  25931  dvlipcn  25955  dvlip2  25956  c1liplem1  25957  dvgt0lem1  25963  lhop1lem  25974  dvcnvrelem1  25978  dvcvx  25981  ftc2ditglem  26008  wilthlem2  27035  dchrval  27201  dchrelbas2  27204  noresle  27665  nosupcbv  27670  nosupno  27671  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd1  27682  nosupbnd2  27684  noinfcbv  27685  noinfno  27686  noinfdm  27687  noinffv  27689  noinfres  27690  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd1  27697  noinfbnd2  27699  noetalem1  27709  norecov  27943  norec2ov  27953  egrsubgr  29350  dfpth2  29802  pthdlem1  29839  eupthvdres  30310  eupth2lem3  30311  eupth2  30314  eucrct2eupth  30320  hhssablo  31338  hhssnvt  31340  hhsssh  31344  fresunsn  32703  fressupp  32767  resf1o  32809  gsummpt2d  33132  gsumpart  33146  symgcom  33165  tocycval  33190  tocycfv  33191  tocycf  33199  tocyc01  33200  cycpm2tr  33201  cycpmconjslem1  33236  cycpmconjslem2  33237  nsgqusf1o  33497  extvval  33696  extvfval  33697  extvfvcl  33701  qtophaus  33993  esumcvg  34243  eulerpartlemn  34538  sseqp1  34552  signsvtn0  34727  ftc2re  34755  reprsuc  34772  bnj1385  34988  bnj1326  35182  bnj1321  35183  bnj1442  35205  bnj1450  35206  bnj1463  35211  bnj1529  35226  f1resfz0f1d  35308  pfxwlk  35318  pthhashvtx  35322  cvmliftlem5  35483  cvmliftlem7  35485  cvmliftlem10  35488  cvmliftlem11  35489  cvmliftlem15  35492  cvmlift2lem11  35507  cvmlift2lem12  35508  satffunlem1lem1  35596  satffunlem2lem1  35598  eldm3  35955  funsseq  35962  finixpnum  37802  poimirlem3  37820  poimirlem4  37821  poimirlem9  37826  sdclem2  37939  prdsbnd2  37992  isdivrngo  38147  drngoi  38148  elrefsymrels2  38822  eleqvrels2  38845  dibffval  41396  hdmapffval  42082  hdmapfval  42083  eqresfnbd  42484  dvun  42610  eldiophb  42995  diophrw  42997  diophin  43010  tfsconcatrev  43586  ofoafg  43592  resisoeq45d  43657  rclexi  43852  rtrclex  43854  rtrclexi  43858  cnvrcl0  43862  dfrtrcl5  43866  dfrcl2  43911  fvmptiunrelexplb0da  43922  sblpnf  44547  fresin2  45412  limsupresuz  45943  limsupvaluz  45948  limsupvaluz2  45978  supcnvlimsup  45980  climrescn  45988  liminfresuz  46024  cncfuni  46126  dvresntr  46158  dvbdfbdioolem1  46168  itgiccshift  46220  itgperiod  46221  dirkercncflem2  46344  fourierdlem46  46392  fourierdlem48  46394  fourierdlem49  46395  fourierdlem58  46404  fourierdlem72  46418  fourierdlem74  46420  fourierdlem75  46421  fourierdlem81  46427  fourierdlem88  46434  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem92  46438  fourierdlem103  46449  fourierdlem104  46450  fourierdlem112  46458  fouriersw  46471  voncmpl  46861  funcoressn  47284  funressnmo  47288  f1cof1blem  47316  funfocofob  47320  funressndmafv2rn  47465  f1oresf1orab  47531  upgrimpths  48151  isubgrgrim  48171  stgrfv  48195  gpgov  48284  rngcidALTV  48516  rhmsubcALTVlem3  48525  funcringcsetcALTV2lem5  48536  ringcidALTV  48550  funcringcsetclem5ALTV  48559  itcoval  48903  itcoval0mpt  48908  itcovalendof  48911  idfu1sta  49342  idfu2nda  49344  imaidfu2  49352  idfullsubc  49402  dfswapf2  49502  oppc1stf  49529  oppc2ndf  49530  1stfpropd  49531  2ndfpropd  49532  fucofvalg  49559  fucof1  49563  fucofvalne  49566  opf2fval  49646  idfudiag1  49766  aacllem  50042