Theorem reseq2d 5950

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

Syntax hints:   → wi 4   = wceq 1540   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921  df-opab 5170  df-xp 5644  df-res 5650

This theorem is referenced by:  reseq12d  5951  imadifssran  6124  resresdm  6206  relresfld  6249  fnunres1  6630  f1orescnv  6815  fococnv2  6826  fvn0ssdmfun  7046  fnressn  7130  fnsnsplit  7158  oprssov  7558  curry1  8083  curry2  8086  dftpos2  8222  frecseq123  8261  fpr3g  8264  frrlem1  8265  frrlem4  8268  frrlem12  8276  fpr2a  8281  wfr3g  8298  dfrecs3  8341  tfrlem16  8361  tfr2ALT  8369  tfr3ALT  8370  on2recsov  8632  sbthlem4  9054  mapunen  9110  hartogslem1  9495  frr3g  9709  frr2  9713  axdc3lem2  10404  fseq1p1m1  13559  resunimafz0  14410  hashf1lem1  14420  relexp0g  14988  relexp0  14989  relexpsucnnr  14991  dfrtrcl2  15028  bpolylem  16014  setsval  17137  idfuval  17838  idfu2nd  17839  resf1st  17856  idfusubc0  17861  idfusubc  17862  setcid  18048  catcisolem  18072  estrcid  18095  funcestrcsetclem5  18105  funcsetcestrclem5  18120  funcsetcestrclem7  18122  1stfval  18152  1stf2  18154  2ndfval  18155  2ndf2  18157  1stfcl  18158  2ndfcl  18159  curf2ndf  18208  hofcl  18220  isps  18527  cnvps  18537  isdir  18557  dirref  18560  tsrdir  18563  frmdval  18778  frmdplusg  18781  gsum2dlem2  19901  dprd2da  19974  dpjval  19988  ablfac1eulem  20004  ablfac1eu  20005  rngcval  20527  rnghmsubcsetclem1  20540  rngccat  20543  rngcid  20544  rngcifuestrc  20548  funcrngcsetc  20549  funcrngcsetcALT  20550  ringcval  20556  rhmsubcsetclem1  20569  ringccat  20572  ringcid  20573  rhmsubcrngclem1  20575  rhmsubcrngc  20577  funcringcsetc  20583  rhmsubc  20598  psrplusg  21845  opsrtoslem2  21963  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  imacmp  23284  ptuncnv  23694  tgphaus  24004  tsmsres  24031  tsmsxplem1  24040  tsmsxplem2  24041  trust  24117  metreslem  24250  imasdsf1olem  24261  xmspropd  24361  mspropd  24362  imasf1oxms  24377  imasf1oms  24378  nmpropd2  24483  isngp2  24485  ngppropd  24525  tngngp2  24540  cphsscph  25151  cmspropd  25249  cmssmscld  25250  mbfres2  25546  limciun  25795  dvmptres3  25860  dvmptres2  25866  dvmptntr  25875  dvlipcn  25899  dvlip2  25900  c1liplem1  25901  dvgt0lem1  25907  lhop1lem  25918  dvcnvrelem1  25922  dvcvx  25925  ftc2ditglem  25952  wilthlem2  26979  dchrval  27145  dchrelbas2  27148  noresle  27609  nosupcbv  27614  nosupno  27615  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd1  27626  nosupbnd2  27628  noinfcbv  27629  noinfno  27630  noinfdm  27631  noinffv  27633  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd1  27641  noinfbnd2  27643  noetalem1  27653  norecov  27854  norec2ov  27864  egrsubgr  29204  dfpth2  29659  pthdlem1  29696  eupthvdres  30164  eupth2lem3  30165  eupth2  30168  eucrct2eupth  30174  hhssablo  31192  hhssnvt  31194  hhsssh  31198  fressupp  32611  resf1o  32653  gsummpt2d  32989  gsumpart  32997  symgcom  33040  tocycval  33065  tocycfv  33066  tocycf  33074  tocyc01  33075  cycpm2tr  33076  cycpmconjslem1  33111  cycpmconjslem2  33112  nsgqusf1o  33387  qtophaus  33826  esumcvg  34076  eulerpartlemn  34372  sseqp1  34386  signsvtn0  34561  ftc2re  34589  reprsuc  34606  bnj1385  34822  bnj1326  35016  bnj1321  35017  bnj1442  35039  bnj1450  35040  bnj1463  35045  bnj1529  35060  f1resfz0f1d  35101  pfxwlk  35111  pthhashvtx  35115  cvmliftlem5  35276  cvmliftlem7  35278  cvmliftlem10  35281  cvmliftlem11  35282  cvmliftlem15  35285  cvmlift2lem11  35300  cvmlift2lem12  35301  satffunlem1lem1  35389  satffunlem2lem1  35391  eldm3  35748  funsseq  35755  finixpnum  37599  poimirlem3  37617  poimirlem4  37618  poimirlem9  37623  sdclem2  37736  prdsbnd2  37789  isdivrngo  37944  drngoi  37945  elrefsymrels2  38560  eleqvrels2  38583  dibffval  41134  hdmapffval  41820  hdmapfval  41821  eqresfnbd  42220  dvun  42347  eldiophb  42745  diophrw  42747  diophin  42760  tfsconcatrev  43337  ofoafg  43343  resisoeq45d  43409  rclexi  43604  rtrclex  43606  rtrclexi  43610  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  fvmptiunrelexplb0da  43674  sblpnf  44299  fresin2  45166  limsupresuz  45701  limsupvaluz  45706  limsupvaluz2  45736  supcnvlimsup  45738  climrescn  45746  liminfresuz  45782  cncfuni  45884  dvresntr  45916  dvbdfbdioolem1  45926  itgiccshift  45978  itgperiod  45979  dirkercncflem2  46102  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem58  46162  fourierdlem72  46176  fourierdlem74  46178  fourierdlem75  46179  fourierdlem81  46185  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fouriersw  46229  voncmpl  46619  funcoressn  47043  funressnmo  47047  f1cof1blem  47075  funfocofob  47079  funressndmafv2rn  47224  f1oresf1orab  47290  upgrimpths  47909  isubgrgrim  47929  stgrfv  47952  gpgov  48033  rngcidALTV  48262  rhmsubcALTVlem3  48271  funcringcsetcALTV2lem5  48282  ringcidALTV  48296  funcringcsetclem5ALTV  48305  itcoval  48650  itcoval0mpt  48655  itcovalendof  48658  idfu1sta  49090  idfu2nda  49092  imaidfu2  49100  idfullsubc  49150  dfswapf2  49250  oppc1stf  49277  oppc2ndf  49278  1stfpropd  49279  2ndfpropd  49280  fucofvalg  49307  fucof1  49311  fucofvalne  49314  opf2fval  49394  idfudiag1  49514  aacllem  49790