Theorem reseq2d 5971

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938  df-opab 5187  df-xp 5665  df-res 5671

This theorem is referenced by:  reseq12d  5972  imadifssran  6145  resresdm  6227  relresfld  6270  fnunres1  6655  f1orescnv  6838  fococnv2  6849  fvn0ssdmfun  7069  fnressn  7153  fnsnsplit  7181  oprssov  7581  curry1  8108  curry2  8111  dftpos2  8247  frecseq123  8286  fpr3g  8289  frrlem1  8290  frrlem4  8293  frrlem12  8301  fpr2a  8306  wrecseq123OLD  8319  wfr3g  8326  wfrlem1OLD  8327  wfrlem4OLD  8331  wfrlem14OLD  8341  wfr2aOLD  8345  dfrecs3  8391  dfrecs3OLD  8392  tfrlem16  8412  tfr2ALT  8420  tfr3ALT  8421  on2recsov  8685  sbthlem4  9105  mapunen  9165  hartogslem1  9561  frr3g  9775  frr2  9779  axdc3lem2  10470  fseq1p1m1  13620  resunimafz0  14468  hashf1lem1  14478  relexp0g  15046  relexp0  15047  relexpsucnnr  15049  dfrtrcl2  15086  bpolylem  16069  setsval  17191  idfuval  17894  idfu2nd  17895  resf1st  17912  idfusubc0  17917  idfusubc  17918  setcid  18104  catcisolem  18128  estrcid  18151  funcestrcsetclem5  18161  funcsetcestrclem5  18176  funcsetcestrclem7  18178  1stfval  18208  1stf2  18210  2ndfval  18211  2ndf2  18213  1stfcl  18214  2ndfcl  18215  curf2ndf  18264  hofcl  18276  isps  18583  cnvps  18593  isdir  18613  dirref  18616  tsrdir  18619  frmdval  18834  frmdplusg  18837  gsum2dlem2  19957  dprd2da  20030  dpjval  20044  ablfac1eulem  20060  ablfac1eu  20061  rngcval  20583  rnghmsubcsetclem1  20596  rngccat  20599  rngcid  20600  rngcifuestrc  20604  funcrngcsetc  20605  funcrngcsetcALT  20606  ringcval  20612  rhmsubcsetclem1  20625  ringccat  20628  ringcid  20629  rhmsubcrngclem1  20631  rhmsubcrngc  20633  funcringcsetc  20639  rhmsubc  20654  psrplusg  21901  opsrtoslem2  22019  mdetunilem3  22557  mdetunilem4  22558  mdetunilem9  22563  imacmp  23340  ptuncnv  23750  tgphaus  24060  tsmsres  24087  tsmsxplem1  24096  tsmsxplem2  24097  trust  24173  metreslem  24306  imasdsf1olem  24317  xmspropd  24417  mspropd  24418  imasf1oxms  24433  imasf1oms  24434  nmpropd2  24539  isngp2  24541  ngppropd  24581  tngngp2  24596  cphsscph  25208  cmspropd  25306  cmssmscld  25307  mbfres2  25603  limciun  25852  dvmptres3  25917  dvmptres2  25923  dvmptntr  25932  dvlipcn  25956  dvlip2  25957  c1liplem1  25958  dvgt0lem1  25964  lhop1lem  25975  dvcnvrelem1  25979  dvcvx  25982  ftc2ditglem  26009  wilthlem2  27036  dchrval  27202  dchrelbas2  27205  noresle  27666  nosupcbv  27671  nosupno  27672  nosupdm  27673  nosupfv  27675  nosupres  27676  nosupbnd1lem1  27677  nosupbnd1lem3  27679  nosupbnd1lem5  27681  nosupbnd1  27683  nosupbnd2  27685  noinfcbv  27686  noinfno  27687  noinfdm  27688  noinffv  27690  noinfres  27691  noinfbnd1lem3  27694  noinfbnd1lem5  27696  noinfbnd1  27698  noinfbnd2  27700  noetalem1  27710  norecov  27911  norec2ov  27921  egrsubgr  29261  dfpth2  29716  pthdlem1  29753  eupthvdres  30221  eupth2lem3  30222  eupth2  30225  eucrct2eupth  30231  hhssablo  31249  hhssnvt  31251  hhsssh  31255  fressupp  32670  resf1o  32712  gsummpt2d  33048  gsumpart  33056  symgcom  33099  tocycval  33124  tocycfv  33125  tocycf  33133  tocyc01  33134  cycpm2tr  33135  cycpmconjslem1  33170  cycpmconjslem2  33171  nsgqusf1o  33436  qtophaus  33872  esumcvg  34122  eulerpartlemn  34418  sseqp1  34432  signsvtn0  34607  ftc2re  34635  reprsuc  34652  bnj1385  34868  bnj1326  35062  bnj1321  35063  bnj1442  35085  bnj1450  35086  bnj1463  35091  bnj1529  35106  f1resfz0f1d  35141  pfxwlk  35151  pthhashvtx  35155  cvmliftlem5  35316  cvmliftlem7  35318  cvmliftlem10  35321  cvmliftlem11  35322  cvmliftlem15  35325  cvmlift2lem11  35340  cvmlift2lem12  35341  satffunlem1lem1  35429  satffunlem2lem1  35431  eldm3  35783  funsseq  35790  finixpnum  37634  poimirlem3  37652  poimirlem4  37653  poimirlem9  37658  sdclem2  37771  prdsbnd2  37824  isdivrngo  37979  drngoi  37980  elrefsymrels2  38592  eleqvrels2  38615  dibffval  41164  hdmapffval  41850  hdmapfval  41851  eqresfnbd  42250  dvun  42377  eldiophb  42755  diophrw  42757  diophin  42770  tfsconcatrev  43347  ofoafg  43353  resisoeq45d  43419  rclexi  43614  rtrclex  43616  rtrclexi  43620  cnvrcl0  43624  dfrtrcl5  43628  dfrcl2  43673  fvmptiunrelexplb0da  43684  sblpnf  44309  fresin2  45176  limsupresuz  45712  limsupvaluz  45717  limsupvaluz2  45747  supcnvlimsup  45749  climrescn  45757  liminfresuz  45793  cncfuni  45895  dvresntr  45927  dvbdfbdioolem1  45937  itgiccshift  45989  itgperiod  45990  dirkercncflem2  46113  fourierdlem46  46161  fourierdlem48  46163  fourierdlem49  46164  fourierdlem58  46173  fourierdlem72  46187  fourierdlem74  46189  fourierdlem75  46190  fourierdlem81  46196  fourierdlem88  46203  fourierdlem89  46204  fourierdlem90  46205  fourierdlem91  46206  fourierdlem92  46207  fourierdlem103  46218  fourierdlem104  46219  fourierdlem112  46227  fouriersw  46240  voncmpl  46630  funcoressn  47051  funressnmo  47055  f1cof1blem  47083  funfocofob  47087  funressndmafv2rn  47232  f1oresf1orab  47298  upgrimpths  47902  isubgrgrim  47922  stgrfv  47945  gpgov  48026  rngcidALTV  48229  rhmsubcALTVlem3  48238  funcringcsetcALTV2lem5  48249  ringcidALTV  48263  funcringcsetclem5ALTV  48272  itcoval  48621  itcoval0mpt  48626  itcovalendof  48629  idfu1sta  49040  idfu2nda  49042  imaidfu2  49050  idfullsubc  49080  dfswapf2  49158  fucofvalg  49209  fucof1  49213  fucofvalne  49216  idfudiag1  49390  aacllem  49645