Theorem reseq2d 5976

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↾ cres 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3909  df-opab 5172  df-xp 5665  df-res 5671

This theorem is used by:  reseq12d  5977  imadifssranOLD  6202  resresdm  6233  relresfld  6277  relresfldOLD  6278  fnunres1  6648  f1orescnv  6837  fococnv2  6848  fvn0ssdmfun  7071  fnressn  7159  fnsnsplit  7186  oprssov  7587  curry1  8105  curry2  8108  dftpos2  8245  frecseq123  8285  fpr3g  8288  frrlem1  8289  frrlem4  8292  frrlem12  8300  fpr2a  8305  wfr3g  8322  dfrecs3  8365  tfrlem16  8386  tfr2ALT  8394  tfr3ALT  8395  on2recsov  8660  sbthlem4  9092  mapunen  9148  hartogslem1  9518  frr3g  9742  frr2  9746  axdc3lem2  10457  fseq1p1m1  13657  f1resfz0f1d  13852  resunimafz0  14514  hashf1lem1  14524  relexp0g  15099  relexp0  15100  relexpsucnnr  15102  dfrtrcl2  15139  bpolylem  16140  setsval  17265  idfuval  17971  idfu2nd  17972  resf1st  17989  idfusubc0  17994  idfusubc  17995  setcid  18181  catcisolem  18205  estrcid  18228  funcestrcsetclem5  18238  funcsetcestrclem5  18253  funcsetcestrclem7  18255  1stfval  18285  1stf2  18287  2ndfval  18288  2ndf2  18290  1stfcl  18291  2ndfcl  18292  curf2ndf  18341  hofcl  18353  isps  18662  cnvps  18672  isdir  18692  dirref  18695  tsrdir  18698  frmdval  18966  frmdplusg  18969  gsum2dlem2  20104  dprd2da  20177  dpjval  20191  ablfac1eulem  20207  ablfac1eu  20208  rngcval  20786  rnghmsubcsetclem1  20799  rngccat  20802  rngcid  20803  rngcifuestrc  20807  funcrngcsetc  20808  funcrngcsetcALT  20809  ringcval  20815  rhmsubcsetclem1  20828  ringccat  20831  ringcid  20832  rhmsubcrngclem1  20834  rhmsubcrngc  20836  funcringcsetc  20842  rhmsubc  20857  psrplusg  22158  opsrtoslem2  22278  mdetunilem3  22842  mdetunilem4  22843  mdetunilem9  22848  imacmp  23628  ptuncnv  24039  tgphaus  24349  tsmsres  24376  tsmsxplem1  24385  tsmsxplem2  24386  trust  24461  metreslem  24594  imasdsf1olem  24605  xmspropd  24705  mspropd  24706  imasf1oxms  24721  imasf1oms  24722  nmpropd2  24827  isngp2  24829  ngppropd  24869  tngngp2  24884  cphsscph  25485  cmspropd  25583  cmssmscld  25584  mbfres2  25879  limciun  26128  dvmptres3  26190  dvmptres2  26196  dvmptntr  26205  dvlipcn  26228  dvlip2  26229  c1liplem1  26230  dvgt0lem1  26236  lhop1lem  26247  dvcnvrelem1  26251  dvcvx  26254  ftc2ditglem  26279  wilthlem2  27313  dchrval  27478  dchrelbas2  27481  noresle  27941  nosupcbv  27946  nosupno  27947  nosupdm  27948  nosupfv  27950  nosupres  27951  nosupbnd1lem1  27952  nosupbnd1lem3  27954  nosupbnd1lem5  27956  nosupbnd1  27958  nosupbnd2  27960  noinfcbv  27961  noinfno  27962  noinfdm  27963  noinffv  27965  noinfres  27966  noinfbnd1lem3  27969  noinfbnd1lem5  27971  noinfbnd1  27973  noinfbnd2  27975  noetalem1  27985  norecov  28220  norec2ov  28230  egrsubgr  29745  pfxwlk  30153  dfpth2  30201  pthhashvtx  30202  pthdlem1  30239  eupthvdres  30723  eupth2lem3  30724  eupth2  30727  eucrct2eupth  30733  hhssablo  31752  hhssnvt  31754  hhsssh  31758  fresunsn  33106  fressupp  33168  resf1o  33209  gsummpt2d  33497  gsumpart  33511  symgcom  33531  tocycval  33556  tocycfv  33557  tocycf  33565  tocyc01  33566  cycpm2tr  33567  cycpmconjslem1  33602  cycpmconjslem2  33603  nsgqusf1o  33853  extvval  34049  extvfval  34050  extvfvcl  34054  qtophaus  34354  esumcvg  34604  eulerpartlemn  34900  sseqp1  34914  signsvtn0  35086  ftc2re  35114  reprsuc  35131  bnj1385  35349  bnj1326  35543  bnj1321  35544  bnj1442  35566  bnj1450  35567  bnj1463  35572  bnj1529  35587  cvmliftlem5  35876  cvmliftlem7  35878  cvmliftlem10  35881  cvmliftlem11  35882  cvmliftlem15  35885  cvmlift2lem11  35900  cvmlift2lem12  35901  satffunlem1lem1  35989  satffunlem2lem1  35991  eldm3  36348  funsseq  36355  finixpnum  38367  poimirlem3  38380  poimirlem4  38381  poimirlem9  38386  sdclem2  38500  prdsbnd2  38553  isdivrngo  38708  drngoi  38709  elrefsymrels2  39409  eleqvrels2  39432  dibffval  42021  hdmapffval  42707  hdmapfval  42708  eqresfnbd  43110  dvun  43242  eldiophb  43610  diophrw  43612  diophin  43625  tfsconcatrev  44197  ofoafg  44203  resisoeq45d  44268  rclexi  44463  rtrclex  44465  rtrclexi  44469  cnvrcl0  44473  dfrtrcl5  44477  dfrcl2  44522  fvmptiunrelexplb0da  44533  sblpnf  45142  fresin2  46012  limsupresuz  46539  limsupvaluz  46544  limsupvaluz2  46574  supcnvlimsup  46576  climrescn  46584  liminfresuz  46620  cncfuni  46722  dvresntr  46754  dvbdfbdioolem1  46764  itgiccshift  46816  itgperiod  46817  dirkercncflem2  46940  fourierdlem46  46988  fourierdlem48  46990  fourierdlem49  46991  fourierdlem58  47000  fourierdlem72  47014  fourierdlem74  47016  fourierdlem75  47017  fourierdlem81  47023  fourierdlem88  47030  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem92  47034  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  fouriersw  47067  voncmpl  47457  tmachlem-agreeself  47772  tmachlem-agreeprod  47773  funcoressn  47938  funressnmo  47942  f1cof1blem  47970  funfocofob  47974  funressndmafv2rn  48119  f1oresf1orab  48185  upgrimpths  48833  isubgrgrim  48853  stgrfv  48877  gpgov  48966  rngcidALTV  49197  rhmsubcALTVlem3  49206  funcringcsetcALTV2lem5  49217  ringcidALTV  49231  funcringcsetclem5ALTV  49240  itcoval  49599  itcoval0mpt  49604  itcovalendof  49607  idfu1sta  50035  idfu2nda  50037  imaidfu2  50045  idfullsubc  50095  dfswapf2  50195  oppc1stf  50222  oppc2ndf  50223  1stfpropd  50224  2ndfpropd  50225  fucofvalg  50252  fucof1  50256  fucofvalne  50259  opf2fval  50339  idfudiag1  50459  aacllem  50780